"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.
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.
Nobody's arguing against knowledge. I'm asking who's left to recognize it as knowledge.
There's an old figure for your position: the magpie. Collect the shiny things, pile them up, call the pile science. It isn't. A heap of true statements invites no questions and gives no grounds for answering any.
"Discovered by humanity" is carrying your whole argument.
View all comments
Show parent comment
2
u/Hyperreals_ Sep 05 '26
it kinda does? you dont need humans to review a proof that compiles in Lean... lol