> Understanding the concrete problem mathematicians are upset about can help us better understand the impact of AI on our own fields,

imo, The author of this essay does not understand the concrete problem that mathematicians are upset about. There is an idea that math [1] and coding [2] are human activities whose purpose is to achieve a certain kind of insight or mental clarity of things. The simplest description of this is by Feyman [3]. AI generated proofs short-circuit human understanding and therefore goes against the primary purpose. The declaration is calling this out loudly to reiterate that the purpose of the endaevor is not the generation and rewarding of proofs.

[1] "On proof and progress in math" https://arxiv.org/pdf/math/9404236

[2] "Programming as theory building" https://pages.cs.wisc.edu/~remzi/Naur.pdf

[3] "What I cannot create, I do not understand"

▲

omnicognate a day ago | parent | next [-]

> But that doesnt mean it is not useful.

If you think the declaration is saying AI is not useful it's you that "does not understand the concrete problem that mathematicians are upset about". Terence Tao uses AI heavily and has been writing extensively about how useful it is ever since it became useful in maths.

▲

xdavidliu a day ago | parent | next [-]

> But that doesnt mean it is not useful

where are you quoting that from? I cannot ctrl-F that in either the article or your parent

	▲	omnicognate a day ago \| parent [-]
		I copied it from the comment I replied to, which has since been edited.

▲

srcreigh a day ago | parent | prev [-]

What do you think the concrete problem is?

▲

omnicognate a day ago | parent [-]

That AI companies are pouring huge resources into strip mining outstanding problems for bragging rights rather than introducing the technology responsibly in a way that benefits the field.

Somebody will now respond that it doesn't matter that it doesn't benefit the field if it can produce the product without the mathematicians, but the whole point is that an LLM-generated Lean proof isn't the product. The proof of a singularity in Navier-Stokes is of zero commercial value (except bragging rights) in itself. If it ever results in something of commercial value it will be far downstream, after any new, valuable ideas in it have been digested, explored, explained, etc. This is work for mathematicians that LLMs cannot (currently) do.

And next someone will respond that LLMs will be able to do that work, however that is a prediction that is yet to come about. It might happen, it might not. To tear down something valuable now on the assumption that it will become obsolete in the future is wildly irresponsible.

▲

fragmede a day ago | parent [-]

I think a million dollars has commercial value, but maybe that's just me.

	▲	nicf a day ago \| parent \| next [-]
		By all accounts this result cost far more than a million dollars to produce, and either way OpenAI announced they won't be accepting the prize.
	▲	omnicognate a day ago \| parent \| prev [-]
		Missing the point by the widest conceivable margin. The million dollars is an award from the Clay Institute. It doesn't represent value in the proof itself, but rather is offered as a reward for an activity that, when done the human way, is expected to result in valuable ideas. As the Clay Institute says on their website, on the Navier-Stokes page: > Why ask for a proof? Because a proof gives not only certitude, but also understanding. It's also a fraction of the amount OpenAI invested in generating the proof, and its value to them is dwarfed by that of "bragging rights".

▲

paimapi a day ago | parent | prev | next [-]

re the Feynman point, couldn't the same argument be said about, for eg, developers no longer manually writing machine code, relying on compilers instead? and the people maintaining those translation layers not knowing the phenomena that results in a transistor flip, trusting the engineering to do what it's said to do? I think an example of the kind of question this leads to would be "do you really understand software if you don't understand electrical engineering and microprocessor architectures?"

there's a level of obfuscation for any knowledge work where you rely on existing but incomprehensible-to-you systems that you just trust to work. are you unable to do any kind of mathematical work if you don't understand every single layer of proof that exists under-the-sun that touches your subject matter - or can you trust that some of these antecedents have been battle-tested and are functionally true for your purpose?

you could make an effective argument about the state of modern general-purpose LLMs that's founded on the idea that they are fundamentally untrustworthy and all results need to be validated but the larger categorical narrative, that the only true way to understand something is to know the logic from the most base principles, seems faulty

	▲	kevindamm a day ago \| parent [-]
		They are different -- higher level languages like C++ and Python surface the abstractions, making them more apparent to the human reading the code. LLMs typically hide the abstractions. You can still read the source code, sure, but even the latest models will produce a lot of repetition of utility functions and produce data structures of various shapes without commonality or reuse. This is moving in the opposite direction that machine code -> assembly -> C -> ... were heading.

▲

arionhardison a day ago | parent | prev [-]

tl;dr - HITL

I think that AI should enhance said proxy.

For example: I have Crohn's so crohns.ai has the entire AGA [gastro.org] and each member is an agent that can participate in my program / protocol.

Same for MNT and dietmanager.com

this is NOT a promo, its a model I am trying to prove; AI can enhance the support that domain experts provide if we remove the barriers.

It's really a matter of AI-native Governance and how we handle that.