Complete list of mathematical theorems and mathematical calc

Stream: general

[Alejandro Lombardo]

12:45 PM

I wish to contribute to the very latest and best version of Lean (proof assistant) but first i need you to send me a complete list of the mathematical theorems and mathematical calculations that the very latest and best version of Lean (proof assistant) can't yet prove or calculate efficiently so that i can teach it how in the most efficient way possible right now. I would appreciate it if you could send me this particular complete list as soon as possible. Thank you for your valuable time and attention and will wait for reply, Alejandro Lombardo

[Damiano Testa]

At any finite time, only a finite number of theorems will have been formalized (or even said out loud by some human being). Since there are countably many theorems that you can formulate, the list that you are looking for will be quite long!

However, grepping lemma and theorem from the .lean files in mathlib will give you a good idea of what is currently formalized!

[Damiano Testa]

Here you can see that there are just under 57000 theorems proven in mathlib.

[Alejandro Lombardo]

Thank you for the insight. Could you please send me the step by step process for accesing lemma and theorem from the .lean files in mathlib as soon as possible? I would appreciate it if you would. Thank you for your valuable time and attention and will wait for reply, Alejandro Lombardo P.S.: Can't wait to start contributing.

[Damiano Testa]

You can find the instructions to install Lean on your computer here.

[Eric Wieser]

Or if you're impatient and want to interact with mathlib immediately, you can use the "gitpod" link in the readme to open everything in-browser.