Get the latest tech news
How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean
- New Frontiers of Mathematics & Computing in Lean lean proof_assistant constructive_mathematics How exactly do mathematicians prove it? – By which I mean, what is the process they use to sit down and write proofs? How do they conjecture lemmas; what problems do they decide to tackle first? and why? While such questions have previously been the subject of much mystery, recent developments, namely at the forefront of mechanised mathematics, is promising to reveal these trade secrets for the first time in history. In particular, I am referring here to the recent interest by prominent mathematicians (such as Terence Tao, Kevin Buzzard, etc.) to formalise, real, novel and cutting-edge mathematical results the Lean Theorem prover.
Below is a visualisation of the evolution of the Lean Blueprint for Terrence Tao's formalisation of the Polynomial Freiman Ruzsa conjecture: (Github URL: https://github.com/teorth/pfr) If you watch for a while you'll see that very often the the graph grows in bursts of yellow bubbles, where presumably some mathematician has sat down and sketched out another part of the proof and broken it down into fragments for others to formalise. Obviously, this is not a particularly deep observation, and was just the result of watching the graph for a bit, but I do think this data is really rich with a lot of previously hidden insights into how these proofs are done.
Or read this on Hacker News
