In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?
by isaacfrond on 3/26/2026, 9:41:44 AM
Comments
by: umutisik
With sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.
3/30/2026, 2:55:01 PM
by: jl6
Imagine a future where proofs are discovered autonomously and proved rigorously by machines, and the work of the human mathematician becomes to articulate the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications. Mathematicians as illuminators and bards of their craft.
3/30/2026, 3:38:39 PM
by: johnbender
I’m confused by the calculus example and I’m hoping someone here can clarify why one can’t state the needed assumptions for roughed out theory that still need to be proven? That is, I’m curious if the critical concern the article is highlighting the requirement to “prove all assumptions before use” or instead the idea that sometimes we can’t even define the blind spots as assumptions in a theory before we use it?
3/30/2026, 2:35:21 PM
by: zitterbewegung
I think the future of having lean as a tool is mathematicians using this or similar software and have it create a corresponding lean code. [1] This is an LLM that outputs Lean code given a mathematical paper. It can also reason within lean projects and enhance or fix lean code.<p>[1] <a href="https://aristotle.harmonic.fun" rel="nofollow">https://aristotle.harmonic.fun</a>
3/30/2026, 2:38:38 PM
by: j45
Is digitized proofs another way of saying the equivalent of a calculator, when a calculator was new?
3/30/2026, 3:57:27 PM
by: riverforest
Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
3/30/2026, 2:33:47 PM
by: ux266478
Rigor was never vital to mathematics. ZFC was explicitly pushed as the foundation for mathematics because Type Theory was too rigorous and demanding. I think that mathematicians are coming around to TT is a bit of funny irony lost on many. Now we just need to restore Logicism...
3/30/2026, 2:07:15 PM