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.
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.
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."
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!
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.
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.
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."