In math, rigor is vital, but are digitized proofs taking it too far?
quantamagazine.org
In math, rigor is vital, but are digitized proofs taking it too far?
1–10 of 112 posts
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#2Rigor 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...
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#3Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#4I’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?
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#5Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
If rigor is the whole point why are we so focused on classical math (eg classical logic) not the wider plurality?
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#6I 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.
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#7Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
Rigor is not the whole point of math. Understanding is. Rigor is a tool for producing understanding. For a further articulation of this point, see
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#8Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
Rigor is one solution to mutual understanding Bourbaki came up with that in turn led to making math inaccessible to most humans as it now takes regular mathematicians over 40 years to get to the bleeding edge, often surpassing their brain's capacity to come up with revolutionary insights. It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the job.
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#9With 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.
Re: In math, rigor is vital, but are digitized proofs taking it too far?
#10I’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?
In calculus the core issue is that the concept of a "function" was undefined but generally understood to be something like what we'd call today an "expression" in a programming language. So, for example, "x^2 + 1" was widely agreed to be a function, but "if x The formal definition of "function" is totally different! This is typically a big confusion in Calculus 2 or 3! Today, a function is defined as literally any input→output mapping, and the "rule" by which this mapping is defined is irrelevant. This definition is much worse for basic calculus—most mappings are not continuous or differentiable. But it has benefits for more advanced calculus; the initial application was Fourier series. And it is generally much easier to formalize because it is "canonical" in a certain sense, it doesn't depend on questions like "which exact expressions are allowed".
This is exactly what the article is complaining about. The non-rigorous intuition preferred for basic calculus and the non-rigorous intuition required for more advanced calculus are different. If you formalize, you'll end up with one rigorous definition, which necessarily will have to incorporate a lot of complexity required for advanced calculus but confusing to beginners.
Programming languages are like this too. Compare C and Python. Some things must be written in C, but most things can be more easily written in Python. If the whole development must be one language, the more basic code will suffer. In programming we fix this by developing software as assemblages of different programs written in different languages, but mechanisms for this kind of modularity in formal systems are still under-studied and, today, come with significant untrusted pieces or annoying boilerplate, so this solution isn't yet available.
[1] Later it was discovered that in fact this set isn't analytic, but that wasn't known for a long time.
[2] I am being imprecise; integrating and solving various differential equations often yields functions that are nice but aren't defined by combinations of named functions. The solution at the time was to name these new discovered functions.