New comment by cmceanga in "“Math 2.0” will need to value mathematical progress more holistically"

cmceanga — Thu, 08 Oct 2026 10:45:10 +0000

There is no guarantee that the lean proof is 1:1 with the natural language equivalent. The lean proof can be lesser. This happened in the Navier-Stokes proof, e.g. see [1] in example 3.1. Having the certificate doesn't necessarily imply correctness.

[1] https://arxiv.org/abs/2610.08144

Hacker News: cmceanga

New comment by cmceanga in "“Math 2.0” will need to value mathematical progress more holistically"