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.
In my experience AI is a very bad teacher. It mumbles in AI-ish, a dialect of English which is difficult to understand without reading things twice. Also, it uses concepts before they are defined. And doesn't have a good mental model of what the reader knows. Stuff like that.
I would think the exact opposite. I always lacked academic rigor and I own that.
How could you come in with less rigor and claim to understand things because you're using AI?. Sorry for the aggressive tone but is there an answer to that questipn?
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 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.
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.
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.
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.
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).
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) formal proofs.
Well since one of the authors of TFA is literally the person who was asked by the association of symbolic logic to give the memorial lecture for Goedel’s centenary the comment could scarcely have been wider of the mark.
Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”
People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...
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."
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.
Only a minor in mathematics here. That's interesting that it struggles with definitions. Maybe unsurprising given the different ways they're chosen and written (motivational, aesthetic, pedagogical, etc)? A big lever to keep hold of.
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.
Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory.
The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."
All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.
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.
AI labs definitely should work on it.
How could you come in with less rigor and claim to understand things because you're using AI?. Sorry for the aggressive tone but is there an answer to that questipn?
...how?
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.
I track blogs because I'm interested in a specific person. I feel disconnect with different style, narration and naming of the new author
Just... make a new blog for new person and start linking posts to each other. C'mon
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.
> “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"
The internal/external logic of sets is exactly where Set gets confusing with computation.
Subsingletons (mere props) being choice theoretic is exactly where we have to resort to HoTT etc..
That shift in limitations from internal vs. external is a lens on many independence results.
Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE
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) formal proofs.
Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”
People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...
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."
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.
The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."
All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.
AI has all the answers. Why read the article?
(The wording may not be exact, though the sense should be.)