How to Formalize All of Mathematics

The current cycle of AI and mathematics gives me great hope for ordinary people like myself to try and attempt learning some mathematics and try and see if I like the experience. Has any one tried that or is trying that? How are you approaching it? I would like to know - you can DM me - I would love to have a conversation if this excites you :)

I think the _key_ to knowing if I can do it has to come from the fact if my intuition about a problem helps me make progress. I would use AI to learn the parts I did not know and engage a community of people to ask questions. Both are key.

Also I am not 100% sure, but me beginning straightaway with lean to try something — like an engineer would — does not seem like the right approach before building some critical mass in the subject. It feels kinda wrong like building the cart before the wheel would.

IMO mathematics benefits from being highly generic compared to normal code, so much so that the implementation itself doesn't really matter (and it's entirely normal in mathematics to skip details, unlike in software). So then to me it makes sense to have a clean separation between basically header files and implementation files like in C and C++. Then something like mathlib should be a pristine collection of what belongs in headers: data structure definitions, instances, theorem statements, macros/tactics for common techniques, etc. So basically it is a curated set of "axioms" that can be used for other math and remain understandable, indexable, etc. Maybe a companion mathlib-full that can actually compile the entire theory.

I suppose this could be done with just tooling to generate a skeleton/index of a giant repository of all mathematics if you decided that you're going to index all definitions and theorems but not lemmas or examples or something like that.

$ChatGPT> "How to Formalize All of Mathematics?"

AI has all the answers. Why read the article?

Reminds me of the following papers (from 1979!) by Ernst Snapper;

1) What is Mathematics? - https://sci-hub.reatk.com/10.2307/2320582

2) The Three Crises in Mathematics: Logicism, Intuitionism and Formalism - https://sci-hub.reatk.com/10.2307/2689412

AI is the fourth crisis in Mathematics!

Formalism has been so successful that the General Public thinks that is all there is to Mathematics. And now AI has made this trivial.

But hopefully, Mathematicians are looking at more foundational and philosophical underpinnings.

Hasn’t this been tried already?

Godel would like to talk to you about his “Incompleteness Theorem”

I like the pragmatic take on AI in mathematics. Running off and proving/formalizing things in incomprehensible ways is marginally useful, and probably harmful for any work that needs to move beyond it. But, there's value in what AI is capable of doing for working mathematicians, when used as a partner.

The genie is out of the bottle though. It's hard to see how there won't be weird and inscrutable branches of mathematics that LLMs build and use effectively _for themselves_, in the same way much of the slop LLMs write in spoken language is really for the consumption of LLMs.

Surely there will be a new kind of research mathematician that's investigating this output in the same way, say, academics in literature read.

Formally verifying all of math would be an amazing achievement by humanity.

If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev

"How to rewrite all software in Rust"

[dead]

[flagged]

[flagged]