Formalizing 100 Theorems | Hacker News Reader

Formalizing 100 Theorems

cs.ru.nl

91 pointsespeed25 comments

I think this list of challenge theorems managed by Freek Wiedijk has encouraged math formalization in general, and been good for all.

That's certainly true for Metamath; once the progress of Metamath was tracked against this list of 100 theorems (around 2014), a lot more theorems from the 100 theorems list were added of course: https://docs.google.com/spreadsheets/d/1jcLOp_jF4sPrVPdPedL_... but in fact more proven theorems were added in general: https://docs.google.com/spreadsheets/d/1TnuBekyUP918smZeJRD0...

Metamath's state is a little amazing; it's tied for third place, yet there is very little built in. For example, numbers are not built-in, they are a derived construct. Metamath didn't even have a decimal number representation until 2015. When you truly start with just logic and set theory (specifically ZFC) it's a lot of work to get to just the basics, especially when you have to directly show every step. Each of the systems listed here are worthy systems. I work most with Metamath; this video I created explains more about its background: https://www.youtube.com/watch?v=8WH4Rd4UKGE

I think mathematical formalization is important, and in the long term that needs to be the direction of mathematics in general. It's too easy to make "proofs" that have errors that slip by. Automated theorem verification systems don't get tired and give far more confidence that proofs really are proofs. If math is all about proving that certain claims can be proven from well-accepted assumptions, then we need to make those proofs more rigorous.

I really like how Metamath sits on an extreme edge; its underlying formalization is simple, to the point where a relatively short Python script [0] is sufficient to do verification, and this also massively increases confidence, at the meta-level, in the correctness of the entire endeavor.

I wonder about how Metamath compares to wholly-constructive approaches common in abstract algebra, category theory, and computer science. I suspect that, much like Archimedes with his levers, a category theorist with a sufficiently-large blackboard could draw a diagram to constructively prove anything that they like, and it's unfortunate that this style of argument is not compatible with current formal methods.

[0] http://us.metamath.org/downloads/mmverify.py

> a sufficiently-large blackboard

And I guess that's where the computer and all of its automation powers enters the picture, right?

I wonder about the status of Raph Levien's Ghilbert [1]. It seemed an approachable proxy to Metamath, promising enough that I thought I can persuade my mathematician friends to look at it sooner or later.

[1] https://ghilbert.org/

Very much agreed, and V. Voevodski has expressed authentic concern from the working mathematician side that peer review needs machine help. Wiedijk writings are nice. I have taken a look at Mizar articles and they are a fantastic sample of good things already achieved. We need to close the usability gap so writing formalizations is just easier. We need a big open source project, the Linux of mathematical vernacular.

"If you wish to make an apple pie from scratch, you must first invent the universe." - Carl Sagan

The equivalent proof in Metamath that the square root of 2 is irrational is here: http://us.metamath.org/mpegif/sqr2irr.html

"The Seventeen Provers of the World" compiled by Freek Wiedijk shows proofs of "the square root of 2 is irrational" in a variety of systems, making it much easier to compare different systems. http://www.cs.ru.nl/~freek/comparison/comparison.pdf

For example, the Metamath system literally shows every step, no exceptions; many other systems only show a program script to enable the computer to re-discover the proof (instead of being the actual proof itself). Which is "better"? Well, that depends on your goals :-). But it's much easier to compare systems by showing an example.

We detached this comment from https://news.ycombinator.com/item?id=18513636 and marked it off-topic.

uh That seems odd, right? Thats the url of this whole page. Please don't post like this again. :-)

Whoops, that was a bug at our end. Sorry!

Sorry for being so cheeky.

In addition to formalising _theorems_, one can aim to formalise _definitions_. See here for some discussion:

https://mathoverflow.net/questions/311071/which-mathematical...

Of course the two are very much intertwined but I think if we're to get serious about formalising mathematics, it would be better to aim to have fully formalised statements of major theorems rather than their proofs for now.

I don't work in this field, but I would like to know out of lay interest. Are there translators that to convert proofs in one system to another? Such a translator would prove (pardon!) to be useful to collaborating researchers.

I know that these systems each have unique features, so I don't mean a 100% translation. For the purposes of this question, translating proofs for the intersection of features would suffice.

There has been some work to translate between systems.

For example, see "Conversion of HOL Light proofs into Metamath" by Mario Carneiro, 2014: https://arxiv.org/abs/1412.8091

However, it turns out to be non-trivial, so it is not typically done in practice. Formalization requires very precise specification, and even slight differences can cause complications. But like many other things, who knows, perhaps there will be further progress in this area.

Does this just mean the theorem has been stated in a formalism, or that there's a machine proof?

The latter, though sometimes you need to follow a few links, and some of them are broken. But there is a proof. Somewhere :-)

The Coq edition appeared recently: https://news.ycombinator.com/item?id=18154140

I’m surprised there is not a clear winner. Are the proof systems so different that one cannot “embed” a proof from one system into another easily?

The ones I'm familiar with avoid Turing-completeness in order to ensure that all functions are total. In doing so, they remain quite expressive but not enough to write interpreters for themselves. So the usually straightforward strategy of embedding a language by writing an AST datatype and interpreter is unlikely to work in this space.

Different systems can have very different logical foundations, so converting proofs from a system to another can be very complicated in general. Even when converting is possible, the converted proof might be very anti-idiomatic in the target system, in more or less the same way one automatically converting Haskell to C is likely to produce very anti-idiomatic C. Also, communities do not necessarily compete for this list.

Keeping this in mind, there still is something:

* OpenTheory (http://www.gilith.com/opentheory/) provides some kind of lingua franca between systems of the HOL family, that are rather similar.

* Mario Carneiro wrote an article (https://arxiv.org/abs/1412.8091) on automatic conversion from OpenTheory to Metamath. I am not aware of an actual implementation.

* Although it is not the same things, some systems have tools that can feed a subproof to an ATP (automated theorem proved) and reconstruct a valid proof to it. That simplifies proof writing.

I did not a comprehensive review, so the list may be lacking.

Has anyone seen a formal proof of different cardinals based on axiomatic set theory? The diagonal argument in particular is very weak imo.

I'm not certain how to interpret what you're asking. However, if what you're asking is how to derive numbers from basic axiomatic set theory, that is certainly available in metamath. An easy to read introduction is here: http://us.metamath.org/mpegif/mmcomplex.html

It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html . The formalization is both short and straightforward, so while you might argue that the axioms of set theory aren't intuitive enough, the fact that they come together to prove the impossibility of bijection between a set and its powerset is unassailable.

I'm glad my suspicion about Haskell is confirmed on account of the complete absence of its mention on that page:

Haskell is an unfortunate contraption of computer science with the primary goal of looking down upon programmers for not knowing enough math, and looking down upon mathematicians for not knowing enough programming.

That page compares proof assistants. Haskell is not a proof assistant and it is not designed to be. I don't think its presence or absence from the list provides any evidence for your opinion about the language.

Reply on news.ycombinator.com