Discussion
In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?
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.
woopwoop: Rigor is not the whole point of math. Understanding is. Rigor is a tool for producing understanding. For a further articulation of this point, seehttps://arxiv.org/abs/math/9404236
gzread: It seems you have never tried to prove anything using a proof assistant program. It will demand proofs for things like x<y && y<z => x<z and while it should have that built in for natural numbers, woe fall upon thee who defines a new data type.
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.
YetAnotherNick: The thing is if something is proved by checking million different cases automatically, it makes it hard to factor in learning for other proofs.
_alternator_: Let’s not forget that mathematics is a social construct as much as (and perhaps more than) a true science. It’s about techniques, stories, relationships between ideas, and ultimately, it’s a social endeavor that involves curiosity satisfaction for (somewhat pedantic) people. If we automate ‘all’ of mathematics, then we’ve removed the people from it.There are things that need to be done by humans to make it meaningful and worthwhile. I’m not saying that automation won’t make us more able to satisfy our intellectual curiosity, but we can’t offload everything and have something of value that we could rightly call ‘mathematics’.
seanmcdirmid: Automating proofs is like automating calculations: neither is what math is, they are just things in the way that need to be done in the process of doing math.Mathematicians will just adopt the tools and use them to get even more math done.
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.
tines: But in this future, why will “the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications” be necessary? Catering to hobbyists?
layer8: Mapping theorems to applications is certainly necessary for mathematics to be useful.
tines: Sure, applications are necessary, but why will humans do that?
