Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

quantamagazine.org

Post reply on HN
Print view View original

21–30 of 112 posts

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

#21

Post by quietbritishjim »

seanmcdirmid wrote: post #20
_alternator_ wrote: post #19

Earlier quoted context omitted.

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 meaningfu…

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.

I don't think that's true. Often, to come up with a proof of a particular theorem of interest, it's necessary to invent a whole new branch of mathematics that is interesting in its own right e.g. Galois theory for finding roots of polynomials. If the proof is automated then it might not be decomposed in a way that makes some new theory apparent. That's not true of a simple calculation.

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

#22

Post 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.

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

#23

Post by tines »

jl6 wrote: post #22

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.

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?

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

#24

Post by layer8 »

jl6 wrote: post #22

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.

The question is whether the capabilities that would let AI take over the discovery part wouldn’t also let them take over the other parts.

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

#26

Post by layer8 »

tines wrote: post #23
jl6 wrote: post #22

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.

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?

Mapping theorems to applications is certainly necessary for mathematics to be useful.

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

#27

Post by 3yr-i-frew-up »

_alternator_ wrote: post #19
umutisik wrote: post #9

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.

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 meaningfu…

[dead]

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

#28

Post by tines »

layer8 wrote: post #26
tines wrote: post #23

Earlier quoted context omitted.

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?

Mapping theorems to applications is certainly necessary for mathematics to be useful.

Sure, applications are necessary, but why will humans do that?

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

#29

Post by ndriscoll »

quietbritishjim wrote: post #21
seanmcdirmid wrote: post #20

Earlier quoted context omitted.

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.

I don't think that's true. Often, to come up with a proof of a particular theorem of interest, it's necessary to invent a whole new branch of mathematics that is interesting in its own right e.g. Galois theory for finding roots of polynomials. If the proof is automated then it might not be decomposed in a way that makes some new theory apparent. That's not true of a simple calculation.

This is literally the same thing as having the model write well factored, readable code. You can tell it to do things like avoid mixing abstraction levels within a function/proof, create interfaces (definitions/axioms) for useful ideas, etc. You can also work with it interactively (this is how I work with programming), so you can ask it to factor things in the way you prefer on the fly.

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

#30

Post by jhanschoo »

seanmcdirmid wrote: post #20
_alternator_ wrote: post #19

Earlier quoted context omitted.

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 meaningfu…

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.

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.

Post reply on HN