Hacker News Reader

Comment by bluecheese452 | Hacker News Reader

Isn’t it more like it merges the code without a dev reviewing or understanding it?

Pretty close, but IMO not quite. A math proof in and of itself is useless unless either:

   (A) it furthers human knowledge
   (B) it gets used in applied sciences, engineering, etc.

If you merge and deploy code, you have released a tool that can be used. If you ship a gibberish math proof, it's not useful unless someone else can understand and deploy it to some other means. Now, it's possible AI could understand and make use of the math proofs, even if we can't, which refutes some of my hair splitting :)

Not necessarily. That's the best case scenario, but proofs can be intrinsically useful in and of themselves. It's just that for problems of that nature, speculative work is often done ahead of time, e.g. the body of work that already exists assuming the Riemann hypothesis is true.

That's a good point!

No. Merged code can perform actions with effects on the world, even if a human being never saw it. Constructing a giant Lean formalization that nobody understands simply doesn't do anything.

Reply on news.ycombinator.com