B LEAN The New Way to Prove Theorems

[jedishrfu]

TL;DR Summary

LEAN is a programming language designed to aid mathematicians in proving any mathematical theorem via a collection of proven theorems.

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/

 

[jedishrfu]

Here‘s a central resource for LEAN programming

https://leanprover.github.io/

 

[mfb]

“It will likely be decades before [Lean] is a research tool,” said Heather Macbeth of Fordham University, a fellow Lean user.

“Coq is an old man now, and it has a lot of scars,” said Mahboubi, who has worked with the program extensively. “It’s been collaboratively maintained by many people over time, and it has known defects due to its long history.”

What could possibly go wrong?

 

[jedishrfu]

The best laid plans of mathematicians and men.

 

[S.G. Janssens]

Thank you for this. I tend to be sceptical about theorem provers, specially in analysis:

These are the ingredients that mathematicians can mix together in Lean to make mathematics. Right now, despite those numbers, it’s a limited pantry. It contains almost nothing from complex analysis or differential equations — two basic elements of many fields of higher math

However, its interesting and good to keep an eye on. Two concerns:

1. Does this involve redoing a substantial amount of the work that already served as input for Coq?
2. If people start to depend on these systems for actual research, then to what extend is the computer's aptness for certain kinds of mathematics going to dictate what sort of problems people will work on?