Hacker News new | past | comments | ask | show | jobs | submit login

I don't know whether or not Lean is the "best" (no doubt that depends on what aspects you think are important). But I completely agree with the speaker that there is a need to formalize mathematics with computer verification. The current "counsel of elders" model of verification is simply not able to verify proofs with any serious level of confidence today, given the explosion of complexity in modern math. This will change how math will be done in the future; we will look back on current math "proofs" in the way we look back on medicine based on the humors (woefully inadequate).

There are, of course, people working on fixing this. I just created a Gource visualization of the Metamath set.mm project, which has been working to formalize mathematics with absolute rigor. Over the years there has been increased activity; there have now been 48 contributors to set.mm.

In the end, that is what is necessary to formalize mathematics: efforts by many people working together to do it.

See: https://www.youtube.com/watch?v=XC1g8FmFcUU

How is interoperability going on between those various formal systems? Couldn't we devise some common intermediate representation, or API?

Some languages (and their approaches) are probably better suited to some mathematical objects, like some demonstrations are easier to perform algebraically than geometrically, for instance.

This turns out to be quite hard, because there are irreconcilable differences in the fundamentals of the different proof systems. That said, there's the Dedukti project, which is showing promising interop results between (at least) Coq and HOL style logics, and the work Mario Carneiro is doing trying to bridge between Metamath and more type-theory approaches.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact