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.

▲

layer8 13 hours ago | parent | next [-]

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.

▲

tines 13 hours ago | parent | prev | next [-]

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?

▲

fasterik 8 hours ago | parent | next [-]

Most mathematicians don't understand the fields outside of their specialization (at a research level). Your assumption that intuition and applications are limited to hobbyists ignores the possibility of enabling mathematicians to work and collaborate more effectively at the cutting edge of multiple fields.

▲

ndriscoll 12 hours ago | parent | prev | next [-]

Very far in the future when AI runs everything, of course math will be a hobby (and it will be great! As a professional programmer I'm happy that I now have a research-level tutor/mentor for my math/physics hobby). In the nearer term, it seems apparent to me that people with stronger mental models of the world are able (without even trying!) to formulate better prompts and get better output from models. i.e. as long as people are asking the questions, they'll do better to have some idea of the nuance within the problem/solution spaces. Math can provide vocabulary to express such nuance.

▲

layer8 13 hours ago | parent | prev [-]

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

▲

tines 13 hours ago | parent [-]

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

	▲	layer8 12 hours ago \| parent [-]
		I agree (https://news.ycombinator.com/item?id=47575890), but the parent assumes that AI will lack the ability.

▲

rtpg 7 hours ago | parent | prev | next [-]

Proofs of what?

Proofs tend to get generated upstream of people trying to investigate something concrete about our models.

A computer might be able to autonomously prove that some function might have some property, and this prove is entirely useless when nobody cares about that function!

Imagine if you had an autonomous SaaS generator. You end up with “flipping these pixels from red to blue as a servis” , “adding 14 to numbers as a service”, “writing the word ‘dog’ into a database as a service”.

That is what autonomous proof discovery might end up being. A bunch of things that might be true but not many people around to care.

I do think there’s a loooot of value in the more restricted “testing the truthfulness of an idea with automation as a step 1”, and this is something that is happening a lot already by my understanding.

▲

thaumasiotes 7 hours ago | parent | prev [-]

> 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

You've got the wrong idea of what mathematicians do now. There's not a proof shortage! We've had autonomously discovered proofs since at least Automated Mathematician, and we can have more whenever we want them - a basic result in logic is that you can enumerate valid proofs mechanically.

But we don't want them, because most proofs have no value. The work of a mathematician today is to determine what proofs would be interesting to have ("compelling motivations"), and try to prove them.