Hacker News Reader

Comment by mittensc | Hacker News Reader

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.

View on HN

there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is.

just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.

The theorem doesn't exist in a vacuum. It talks about objects that must be formally defined. And if that formal definition (which is part of the API) is not immediately compatible with those others use, and every single theorem comes with its own definitions of the objects they're working on, you're going to be reinventing the wheel over and over again.

Replacing thought and curation with repeated automation is tech debt, pushed down to fundamental knowledge and understanding.

> just as we don't re-prove Fermat's little theorem every time I use it in a proof

Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface.

But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfully repurpose the individual Lego blocks to build a different interface. You end up having to reinvent the same Lego blocks over and over again, just with a slightly different color each time.

Don't want to re-prove each and every Lego brick? Then you shouldn't accept giant black box proofs.

I think the interesting part here is that the black box gives us a starting point. And it's not a true black box: if a model is generating Lean, we can examine the entire source, iteratively refine by refactoring into smaller self-contained units, and the compiler gives us the certainty that our decomposition is correct.

I just wanted to commend you on this analogy. Very nice. Thank you!

Reply on news.ycombinator.com