You are conflating:

(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.

Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.

Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.

You can't deny it if it's true, but the point is to find new techniques and abstractions. A proof you can't extrapolate and learn from is just a checkmark, and about as useful.

There's a difference in math between giving just the answer to a problem and doing it properly/elegantly.

So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.

> I see no reason not to accept the vibe coded blob if Lean says it's kosher except anthropocentrism.

The laws of mathematics exist and their truths hold before they are proven by humans or our machines, so in a very real sense the entire point of proving anything in the first place is anthropocentrism.

That, plus cleaning it up may reveal it contains proofs of other things we also want to know. Imagine if this happened to also contain as a sub-part a proof of all the open Millennium Prize Problems? We don't know until we investigate. (If it was a specific list of things to check from rather than expanding humanity's library, we could just ask an AI to do it for us… but as The Wachowski sisters wrote in their most famous script: "I say your civilization because as soon as we started thinking for you, it really became our civilization").

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct. But you gotta check.

This future of "the AI built the compiler and it's totally incomprehensible spaghetti, but don't worry, it verified the compiler works using this AI-generated proof assistant whose codebase is also pure spaghetti" terrifies me.

You might get the Riemann hypothesis robo-proven and unintelligibly dense. Would mathematic professionals trust it, or would they always be putting asterisks next to proofs downstream of it ?

>But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me.

Why not just fork the original master branch of human science to an ai-enhanced one and see where that brings us?

> Imo, the proved theorem is the API. And that's really all it has to be.

The novel approaches to solving challenging proofs is very useful.

But part of the point of mathematics is human understanding. I think most would be willing to accept the proof. They just wouldn't think it's nearly as useful as one that could be understood.