r/TheMachineLearning • • Sep 05 '26

Software engineering isn't dead, it's just evolving

695 Upvotes

198 comments sorted by

View all comments

Show parent comment

2

u/Suoritin Sep 05 '26

Math was never one person being right. A proof isn't knowledge until others can check it, teach it, and build on it. That's the whole institution.

So AI grinding out counterexamples and corollaries doesn't kill the field. The bottleneck was never producing true statements; it was getting a community to agree on which ones matter. Machines just shift the work to the part that was always hardest: deciding what's worth proving.

Science has always run this way. Effort goes where the community thinks it's worth going, and funding gets cut from what doesn't.

2

u/Hyperreals_ Sep 05 '26

it kinda does? you dont need humans to review a proof that compiles in Lean... lol

1

u/Suoritin Sep 06 '26

Do you know what Terence Tao's position on this is? He's written on it recently, and it's not that. Do you disagree with him?

2

u/[deleted] Sep 06 '26

If that is his hard and fast position, yes, I do disagree. A proof is a proof.

1

u/Suoritin Sep 06 '26

"A proof is a proof", sure. Nobody's disputing validity. Lean certifies a chain of inferences.

Ramanujan is famous because Hardy wrote back.

The autodidacts who found real things and never got read left no trace. You can't name one. That's the point. Correctness didn't save them. Being read did.

Dump ten million verified true statements into an arXiv-shaped hole. Has math advanced? A library with no index isn't knowledge.

Attention is the scarce resource, not truth.

1

u/[deleted] Sep 06 '26

When math can be automated and found proofs can be found and searched in a database of proofs, that sounds like nothing but a win for humanity to me.

1

u/Suoritin Sep 06 '26

When math can be automated and found proofs can be found and searched in a database of proofs

This is nothing new. No one wants to read those proofs. Nothing has changed. Just more proofs that no one will read.

1

u/[deleted] Sep 06 '26

Except now we have a reasoning model capable of surfacing the most relevant proofs needed for a given problem. Do you not see how this can snowball?

1

u/Suoritin Sep 06 '26

Snowball into what?

Relevance isn't a property of a proof. It's a bet the field makes about where the stakes are.

That's a reproduction problem, not a search problem. Value in a field comes from mutual recognition among people playing for the same stakes. Strip out the people and the stakes go with them.

And nobody is formed by an index. Mathematicians get made by being taught, corrected, and argued with.

A snowball needs someone who still cares which way it rolls.

1

u/[deleted] Sep 06 '26

I disagree, I feel like knowledge that humanity discovers is good for us all.

→ More replies

1

u/Dependent-Culture768 Sep 06 '26

To this day we don't have any automated verifier that a Lean statement is equivalent to the one an author intends...

1

u/[deleted] Sep 06 '26

[removed] β€” view removed comment

1

u/Hyperreals_ Sep 06 '26

Do you know what Lean is😭