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.
The problem with trusting AI to learn a complex subject, which I've tried multiple times, is it will always at some point confidently give you the wrong explanation for something important and you will have no way to detect it. Its quite frustrating and that realization might not come for hours or days and you've built lots of false mental models that can be hard to untangle.
You have to do it along with some sort of ground truth, like a book, and you have to be able to understand that book in order to be able to see that bad advice immediately.
Alas, there are no shortcuts in life. You still need to very eagerly read and understand the source materials you're studying as you would have before AI and to the extent which AI is helpful for that is debatable. Your brain still has to do the thinking.
I can chime in about this. I’m a software engineer and about 7 years ago I decided to get a masters in pure mathematics. Because I was working full time, I could not attend any class so I self studied from textbooks and it worked well.
When I would get stuck, I would struggle with the problem, ask around, ask on Math Stackexchange and along the process I would end up learning a lot more.
With AI now, it’s like having your own tutor: you can ask personalized questions and it would answer it very well.
But that would also mean the amount of time I would spend struggling would go down considerably.
So you really have to be self disciplined and struggle with the problem a little bit before asking for help. You can also ask it to give hints only.
Do not mistake understanding the answer with learning something rigorously.
So if you are curious and doing an exposition, use it as you would normally and it will work wonderfully.
But if you want to learn it rigorously, our usual present habits with AI spitting out answers and us reading them will not work at all.
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.
That makes me imagine a future where various languages import their core data structures and algorithms from a common, language-agnostic "standard library" of mathematically rigorous foundation.
Indeed, what I'd like is formal mathematics proving language that could be viewed as an outline in that natural language math proofs are structured as outlines. The reader would be able to choose what to view - definitions, theorems, lemmas, examples, key-steps, all steps etc.
Ideally, a view would let a reader expand into not just the proof at hand but the various theories in the repository.
A reader could even tell their viewing preferences and it might strip down the UI for those purposes.
The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.
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.
We research mathematicians are still learning how to use AI in research and how to deal with the output. I drafted eight papers last weekend. This week I advanced on none. AI still gets stuck at the key point on a problem where there isn't already a lot of work done. What falls is where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it - and the dominos fall.
So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.
What's not clear is how the professional infrastructure will survive. Journals seem likely to die. The arxiv is swamped. A human can't assess the volume of the output. Serious conjectures have fallen and serious people have checked them.
We are looking for constructive and productive and socially useful ways forward. One reflection is that a lot of what we have been doing was maybe not so interesting as we thought.
This is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable.
They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.
To the extent the theorems in question are impossible to formalize this means the original proof must be in error.
>To the extent the theorems in question are impossible to formalize this means the original proof must be in error.
Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.
That said, I agree with the sentiment that dismissing the entire article on the basis of the incompleteness theorems is shallow and the article is not about formalizing "all" of mathematics in the strict sense. It's mostly about introducing formal tools to the everyday mathematics.
The incompleteness theorem doesn’t mean it’s impossible to formalize all of mathematics. It just means you’ll need to build out “various” mathematics from a landscape of axioms that are not necessarily all compatible with each other.
As the silliest example of this: the Calculus of Inductive Constructions (the core calculus implemented in Lean) has a published proof of its soundness (that you cannot derive False in it). That proof can (probably, thanks to Gödel) not be formalized in Lean or any formal system of axioms weaker than Lean.
If what you were trying to do was define what it means for something to be a correct proof, then you must equally admit that there can't be a correct proof of the fact that Lean can't prove False. And if you find that world a happy world to live in while we delegate all concerns about truth to Lean, then I have an infinite hierarchy of monotonically growing bridges to sell you.
There is no unconditional proof that CIC is sound. Thanks to Gödel, the best you can do is relative consistency proofs, something like "in ZFC with omega (i.e. infinitely) many inaccessible cardinals, you can prove that the theory of Lean is consistent".
Such a relatively consistency proof can be fully formalized in Lean (and in fact, in much weaker systems than Lean).
Any proof which is correct can be formalized. That is what is means for a proof to be correct.
I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms.
In principle, a computer can check a nonconstructive proof. I don't know if that's possible in Lean. The interpretation of proofs still assumes the consistency of their axioms.
Do you honestly Jeremy Avigad (to pick one of the authors) isn't intimately familiar with the Incompleteness Theorems? For starters, Jeremy is chair in logic and philosophy of maths at CMU. https://www.andrew.cmu.edu/user/avigad/
Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?
I think the comment was poking fun at the phrase, "to formalize all of mathematics".
That makes it sound like all possible mathematics past and future in all conceivable worlds. And we already know there are undecidable or unprovable statements, higher-order logics that cannot be fully formalized, concepts about axioms themselves that cannot be axiomatized, etc.
So it cannot mean "all of mathematics", strictly speaking. Just the areas in existing mathematics that have (or can have) proofs.
I understand that, even taking Gödel's results into account, formalization helps us analyze mathematics and can lead to new (non-mechanical) ideas and results.
Yeah which is why I don't have much sympathy for folks like Tao either
The ability to conjure math is practically as endless as time
At some point the outcome is just generation of new visual art in the form of syntax
We can't physically observe the past or future so we can only theorize and simulate; IMO that's the physical phenomena that belies Incompleteness Theorem; from Earth in the relative year of 2026 my view of the universe is fundamentally incomplete. As such all language describing too far either is incomplete always.
It makes any kind of longtermism, religious or agnostic framework espoused by kids of rich academics, empty. We all gonna stick around 10 more generations just to make sure?
Whole lot of educated people are just peddling euphemism for religious conviction they steeped in as kids but hid behind atheist semantics like "Intelligent Design."
The thing is that logicism and formalism were both essentially successful - Godel might thrown a wrench into Hilbert's plans but correcting for the incompleteness problem, a formal process can go forward. Intuitionism was a failure in the sense that just the existence of computers shows
The thing is, I think mathematics as a whole has reached a bit of the sort of crisis that mathematical foundations reached after Godel's theorem. I think Raymond Smullyan said something like (paraphrasing)"We know the continuum hypothesis is independent, it can't be proven or disproven by other hypotheses, we're not trying to do that. But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted".
Mathematicians now can cruise through a huge area of "what can be mechanically deduced/mechanically constructed" and it seems like the task becomes highlighting what matters to us (as humans or mathematicians or some community) within that realm.
If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.
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.
You have to do it along with some sort of ground truth, like a book, and you have to be able to understand that book in order to be able to see that bad advice immediately.
Alas, there are no shortcuts in life. You still need to very eagerly read and understand the source materials you're studying as you would have before AI and to the extent which AI is helpful for that is debatable. Your brain still has to do the thinking.
When I would get stuck, I would struggle with the problem, ask around, ask on Math Stackexchange and along the process I would end up learning a lot more.
With AI now, it’s like having your own tutor: you can ask personalized questions and it would answer it very well.
But that would also mean the amount of time I would spend struggling would go down considerably.
So you really have to be self disciplined and struggle with the problem a little bit before asking for help. You can also ask it to give hints only.
Do not mistake understanding the answer with learning something rigorously.
So if you are curious and doing an exposition, use it as you would normally and it will work wonderfully.
But if you want to learn it rigorously, our usual present habits with AI spitting out answers and us reading them will not work at all.
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.
Ideally, a view would let a reader expand into not just the proof at hand but the various theories in the repository.
A reader could even tell their viewing preferences and it might strip down the UI for those purposes.
Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE
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.
So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.
What's not clear is how the professional infrastructure will survive. Journals seem likely to die. The arxiv is swamped. A human can't assess the volume of the output. Serious conjectures have fallen and serious people have checked them.
We are looking for constructive and productive and socially useful ways forward. One reflection is that a lot of what we have been doing was maybe not so interesting as we thought.
Is it though? We're not benchmarking how well LLMs 'like' it, and slop is characterised by an unnatural absence of useful information.
It seems mostly designed to mislead humans into believing it was written by someone knowledgeable on the subject.
They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.
To the extent the theorems in question are impossible to formalize this means the original proof must be in error.
Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.
That said, I agree with the sentiment that dismissing the entire article on the basis of the incompleteness theorems is shallow and the article is not about formalizing "all" of mathematics in the strict sense. It's mostly about introducing formal tools to the everyday mathematics.
A bit like a multiverse of mathematics.
As the silliest example of this: the Calculus of Inductive Constructions (the core calculus implemented in Lean) has a published proof of its soundness (that you cannot derive False in it). That proof can (probably, thanks to Gödel) not be formalized in Lean or any formal system of axioms weaker than Lean.
If what you were trying to do was define what it means for something to be a correct proof, then you must equally admit that there can't be a correct proof of the fact that Lean can't prove False. And if you find that world a happy world to live in while we delegate all concerns about truth to Lean, then I have an infinite hierarchy of monotonically growing bridges to sell you.
Any proof which is correct can be formalized. That is what is means for a proof to be correct.
I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms.
Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?
That makes it sound like all possible mathematics past and future in all conceivable worlds. And we already know there are undecidable or unprovable statements, higher-order logics that cannot be fully formalized, concepts about axioms themselves that cannot be axiomatized, etc.
So it cannot mean "all of mathematics", strictly speaking. Just the areas in existing mathematics that have (or can have) proofs.
https://ia801804.us.archive.org/35/items/A-Z_Library_G-K_Jos... (PDF)
The ability to conjure math is practically as endless as time
At some point the outcome is just generation of new visual art in the form of syntax
We can't physically observe the past or future so we can only theorize and simulate; IMO that's the physical phenomena that belies Incompleteness Theorem; from Earth in the relative year of 2026 my view of the universe is fundamentally incomplete. As such all language describing too far either is incomplete always.
It makes any kind of longtermism, religious or agnostic framework espoused by kids of rich academics, empty. We all gonna stick around 10 more generations just to make sure?
Whole lot of educated people are just peddling euphemism for religious conviction they steeped in as kids but hid behind atheist semantics like "Intelligent Design."
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.
The thing is, I think mathematics as a whole has reached a bit of the sort of crisis that mathematical foundations reached after Godel's theorem. I think Raymond Smullyan said something like (paraphrasing)"We know the continuum hypothesis is independent, it can't be proven or disproven by other hypotheses, we're not trying to do that. But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted".
Mathematicians now can cruise through a huge area of "what can be mechanically deduced/mechanically constructed" and it seems like the task becomes highlighting what matters to us (as humans or mathematicians or some community) within that realm.
(The wording may not be exact, though the sense should be.)