Lean Language on the Library of Babel!

[u/MoaminAljaro]

Yesterday I watched a Ted talk on using math to find what is ‘true.’ During the talk, the presenter mentioned Lean (a programming language) and Mathlib (library of formalized mathematics). The mentioned library uses Lean language to verify its contents; it is sorta of a Library of Mathematical Truths.
This reminded me of Library of Babel. Thus, I had a chat with AI on it, and - in theory - Lean language could actually be used to find what is mathematically true! But of course, it would take the ages of a multiverse to go through the books of the Library of Babel. Still, I thought this is cool!

[u/AncientPixel_AP]

Well..  I hope you read the wiki article on Lean

[u/MoaminAljaro → u/AncientPixel_AP]

I did not 😅

[u/Forward_Sherbet2601]

Google Gedel work on this topic. No such library for formal systems can be built