Hacker News Front Page · remywang ·
Wir müssen wissen – wir werden wissen
El texto sostiene que la IA y los asistentes de pruebas formales hacen realidad parte del ideal de Hilbert, pero que delegar la producción de código sin leerlo supone renunciar a comprender los sistemas que construimos. Relaciona los programas con las pruebas matemáticas mediante la correspondencia de Curry-Howard y propone simplificar, refactorizar y usar mejores abstracciones hasta que el código generado por IA pueda entenderse.
100 years ago, the world of mathematics experienced a foundational crisis: the identification of several paradoxes revealed cracks in the pillars supporting all areas of math. The most famous of which is Russel’s paradox, which points to the contradictory “set of all sets that do not contain themselves”, thereby showing the inconsistency of naive set theory. This had spurred mathematicians to search for a rigorous foundation for math without contradictions. In particular, David Hilbert initiated a program to design a system of axioms that are complete and consistent, meaning one should be able to derive all mathematical truth from the axioms, while avoiding paradoxes—“the truth, the whole truth, and nothing but the truth”. Such a goal was natural for mathematicians, as it would place their work on firmer grounds. It was therefore also a seismic event when Gödel dealt the death blow to Hilbert’s program with his incompleteness theorems: such a complete, consistent system for math cannot exist!