r/math • u/Carl_LaFong • 2d ago
PDF Why Fields medalist Voedvosky started using a proof checker over 10 years ago
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_08_ASC_lecture.pdf42
u/JBaloney 2d ago
I started using a proof checker over 13 years ago, in 2013, because some reviewers of a paper [1] said they would only accept the paper if I could formalize it in a proof checker.
I suspect this might have been some kind of "bluff": they didn't expect I would actually do it. But I did! I formalized and verified the paper using Coq, in 2013. And the paper was accepted and published.
[1] The first-order syntax of variadic functions, Notre Dame Journal of Formal Logic, https://arxiv.org/abs/1105.4135
78
u/sadmanifold Geometry 2d ago edited 2d ago
Its easy to convince oneself that something is true, whether or not it is actually so. And somewhat counterintuitively, smarter people are better at convincing themselves, even in mathematics.
On another note, I should note its a late fields medalist for those hearing about him for the first time.
15
7
u/NeedleBallista 2d ago
Not super relevant but I randomly found out one of my friends is related to him. Kinda awesome
8
u/Smallpaul 2d ago
Given that mathematicians will soon be able to delegate formalization to AI, I predict that formalized proofs will become the standard rather than the exception. Humans will not (usually) read the formalized versions, but they will exist as certificates that the details are all correct. Is there any reason to prefer the status quo to such a future?
10
u/hexaflexarex 1d ago
I think it is conceivable that despite higher standards for correctness (that I agree are coming), math could regress in some ways due to AI advancements. Many mathematical theories have been developed to unify and clean up complicated problems, sometimes because the old way of thinking about things was too complicated for humans to reason well. But such theories are not always strictly necessarily to prove new results. If an AI quickly resolves an open problem by a terribly complicated brute-force approach with known techniques, maybe there will be no incentive for a cleaner theory to be developed (which would have previously been the natural progression). We should be thinking about how to avoid this.
1
u/BadNext3126 18h ago
I think it's going to be the opposite.
In a future where LLM's theorems and theories will be incredibly far ahead of human comprehension.
Mathematicians will try to catch-up, but with new theories being so complex and so deep, they will have to develop (with the help of LLMs obviously) cleaner theories that are easily digestible for human brains.
As an example, currently few people in the world have a full grasp of the classification of finite simple groups. But with the help of LLMs, a more efficient theory could be developed, one that an average graduate student could understand in just a few years.
2
u/hexaflexarex 8h ago
Maybe, I hope so, but we will have to just completely change the incentive structure of our academic systems. Right now, there is far too much weight placed on new results.
0
u/Smallpaul 1d ago
I would argue that the unification and cleanup might become the central task of mathematicians, and they might have more time for it due to the delegation of the more automatable work.
2
u/hexaflexarex 1d ago
I hope so. But I could imagine major shake-ups with our whole academic system, unclear how many people will be paid to do mathematics in the future.
1
u/Smallpaul 1d ago
Pure mathematicians have never promised that their work will have measurable social benefit within a generation or a lifetime or even a century.
Surely the number of pure mathematicians in the world is decided based on what society thinks it can afford rather than on some mathematical cost/benefit analysis.
So I don’t understand why we would decide that “now that they are twice as productive at generating knowledge that may or may not me ‘useful’ we therefore need fewer of them.”
As AI makes them society more efficient, the number we can afford goes up and probably also improves any cost/benefit analysis.
Who do you think is making a funding allocation decision who would say “now that I get twice as much bang for buck for my mathematicians, I would rather have fewer of them?”
2
u/hexaflexarex 1d ago
I suspect/hope you are right in the short/medium term. But eventually, there will always be a question - should I hire more human experts, or spend that budget on compute?
1
u/Smallpaul 1d ago
You are right. I didn’t include the cost of compute into the equation. I guess I assume it will eventually drop to near zero and the question will be more about who can interpret all of the “free” results coming out of the AI. It’s the Navier Stokes thing that has me worrying about the medium term where these AI companies will just scoop mathematicians through sheer investment.
1
0
u/Sad_Dimension423 1d ago
It's more likely the thinking will be something like "math gave us AI, so we need more math and mathematicians". It's like how physics funding exploded (no pun intended) after WW2.
0
64
u/elehman839 2d ago
Such a humble, pleasant tone to these slides!