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!