In math, rigor is vital, but are digitized proofs taking it too far?

Post by jhanschoo » Wed, Apr 01, 2026, 6:47 AM UTC

seanmcdirmid wrote: post #87

jhanschoo wrote: post #30

Earlier quoted context omitted.

There are areas of mathematics where the standard proofs are very interesting and require insight, often new statements and definitions and theorems for their sake, but the theorems and definitions are banal. For an extreme example, consider Fermat's Last Theorem. Note on the other hand that proving standard properties of many computer programs are frequently just tedious and should be automated.

Yes, but > 90% of the proof work to be done is not that interesting insightful stuff. It is rather pattern matching from existing proofs to find what works for the proof you are currently working on. If you've ever worked on a proof for formal verification, then its...work...and the nature of the proof probably (most probably) is not going to be something new and interesting for other people to read about, it is just…

You're right, I misread your comment. Apologies.

Post by DoctorOetker » Thu, Apr 02, 2026, 3:32 AM UTC

WhitneyLand wrote: post #51

Great quote from Hilbert, I think it’s also a useful thought for software development. “The edifice of science is not raised like a dwelling, in which the foundations are first firmly laid and only then one proceeds to construct and to enlarge the rooms,” the great mathematician David Hilbert wrote in 1905 (opens a new tab). Rather, scientists should first find “comfortable spaces to wander around and only subsequent…

Hilbert's quote is entirely out of context:

1) while many formalists in his day were stress-testing definitions for unexpected gotcha's; some vocal minority were doing formalization as an eccentric art form.

2) commoditized computers running verification software was not available in his day and age

As long as the weakest link was reliance on human brains faithfully attempting to maintain consistency anyway, then it was more productive and fruitful for the economy to focus on translating observations into the language of mathematics.

Once commoditized hardware and minimalistic verification software becomes available, it makes sense to step back and start a machine readable formalization program to translate or verify the main body of mathematics.

Quoting mathematicians of the caliber like Hilbert in 2026 doesn't mean its great guidance in the face of questions Hilbert was never confronted with: with cheap affordable compute, and an enormously expanded number of mathematicians, perhaps its time to formalize the bulk of mathematics.

And it could happen quickly.

A government can mandate that a certain fraction of student scores is assessed on their formalization tasks. Basically turn the job of formalizing mathematics into homework exercises for students. There are students at all levels, undergraduate, graduate, ... If a result isn't proven yet, turn into a temporary axiom, which goes to the collective TODO list.

In a few years all of mathematics that is regularly touched on in academia could be formalized.

Nation states that enforce this will have a large number of mathematicians capable of formalizing systems into machine readable form, and will benefit tremendously compared to nation states that don't (even if the resulting formalizations were public domain: having a sword available is not the same as having workers experienced in smithing such a sword).

Re: In math, rigor is vital, but are digitized proofs taking it too far?

Re: In math, rigor is vital, but are digitized proofs taking it too far?