Why formalize mathematics

Stream: maths

[Patrick Massot]

Stimulated by the release of Kevin's ICM draft, I forced myself to TeX the expanded written version of my Harvard talk. You can find it here. The main reason it has taken so long to appear, while several of you, including Kevin, saw early drafts a while ago, is I don't quite know what to do with this text. For now I simply put it on my webpage. Comments and corrections are very welcome.

[Patrick Massot]

Here is one question for the knowledgeable people in the assistance: is there a good paper or blog post or whatever that can be cited to explain how we can trust a computer program to check proofs while everybody knows computer programs are full of bugs? This would include the concept of small kernel vs tactic framework and independent external checkers. This is not the topic of this paper but having something to cite would be very helpful since this is such a natural question to ask.

[Eric Taucher]

(deleted)

[Eric Taucher]

cognitive dissonance One of my favorite phrases. :grinning:

[Johan Commelin]

@Patrick Massot Might this be what you want?

Pollack, "How to believe a machine-checked proof": http://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf

[Michael R Douglas]

Patrick, we can post this with the video of your seminar if you like.

[Patrick Massot]

Thanks Johan, this seems to be a good starting point.

[Patrick Massot]

Michael, maybe you can put a link to this file next to the video indeed.

[Scott Morrison]

In the abstract: s/loosing/losing/.

[Scott Morrison]

I would be a bit wary of "frightened" and "fear", just on the principle that people don't like being told they are frightened. Perhaps "wary", which has less negative connotation? But if you want fighting words, they are perfect. :-)

[Scott Morrison]

Somewhat off-topic, I was just saying to Johan how much I dislike the label "formalization". Certainly it's okay for some aspects of what we are doing, but I think is --- correctly --- highly off-putting to many outsiders.

[Scott Morrison]

We're not just in the business of boiling down normal mathematics to excessively formal statements close to the axioms, but many many mathematicians immediately think this when hearing "formalization".

[Scott Morrison]

I don't know what to replace it with. But I like things like "proof-assistant enabled mathematics", or if you want an even broader tent "computer augmented mathematics" or even "transhuman mathematics" (which has its own off-putting problems). :-)

[Scott Morrison]

s/in a slight weird but/in a slightly weird way but/, s/readble/readable/, s/and pretend this/and pretending this/, s/in students writings/in students' writings/`

[Johan Commelin]

Last sentence of abstract: s/apply/applies/

[Yury G. Kudryashov]

Computer readable mathematics?

[Adam Topaz]

Why not simply "computer verified mathematics". That doesn't sound negative or off-putting at all to me.

[Patrick Massot]

Thanks Scott. I'm not sure what to do with this "fear sentence". I even considered adding "pretend to be frightened". My target here is Michael Harris, but I don't want to advertise his non-sense ramblings.

[Patrick Massot]

About formalization, I don't have a better word. I hope the whole text explains what it means. "Computer verified mathematics" clearly puts way to much emphasis on the correctness goal.

[Arthur Paulino]

Maybe "computer reasoned mathematics"?

[Kevin Buzzard]

21st century mathematics ;-)

[Arthur Paulino]

For me, personally, what first blew my mind was seeing a computer check that $a+b=b+a$ in a fraction of a second (without having to check for all pairs of $a$ and $b$, I mean).

It stroke me that there was something deep going on and I had no clue about what was happening.

[Jeremy Avigad]

Somewhat off-topic, I was just saying to Johan how much I dislike the label "formalization".

I share the concern, though I also don't see a better alternative. Like Kevin, I prefer "mathematics." I often compare formalization to typesetting; the technology we are using is just a tool to help us do mathematics better, not an end in and of itself. We need to keep saying that over and over until people listen. "Digital mathematics" or "digitized mathematics" emphasizes that it is just a matter of putting mathematics in a certain format so that we can do useful things. "Computer-assisted mathematics" is pretty broad but, I think, also has the right connotations.

When it came to naming, I considered proposing various alternatives to "The Hoskinson Center for Formal Mathematics," like "The Hoskinson Center for Formal Methods in Mathematics" or "The Hoskinson Center for All the Useful Things That Formal Methods and Software Tools Can Do For Mathematics." In the end, we decided that it's hard to beat a short, punchy title, but hopefully it won't obscure the overarching goals.

[Patrick Massot]

This naming issue is difficult, but I think the main point is first to make sure people don't confuse different things, especially computer algebra systems and proof assistants and, less crucially, ITP with ATP. So we need a non-ambiguous word, and formalized mathematics seems ok. It can bring the wrong connotation, but here our task is very clear: we must work on making the science fiction parts of my essay real and easy to understand. Then people will get the correct idea, whatever the name (as long as it's not ambiguous).

[Patrick Massot]

And I think the urgent parts are still the same:

• having a nice range of impressive formalization achievements in a nice range of mathematical topics, including stuff that look difficult to formalize
• work on the dream described in Section 2 of my text

[Patrick Massot]

About the second point, we may seem stuck until mathlib for Lean 4 is there, since working on this within Lean 3 meta-programming framework seems stupid given the circumstances. But I hope that @Niklas Bülow will have news for us before the big switch (he seems to be actively working).

[Eric Wieser]

I look forward to Scholze's blog post in 2022 (the last reference)

[Patrick Massot]

This whole business is all about anticipating our bright future.

[Adam Topaz]

Patrick Massot said:

About formalization, I don't have a better word. I hope the whole text explains what it means. "Computer verified mathematics" clearly puts way to much emphasis on the correctness goal.

I completely understand your point here, Patrick, but what this highlights, which I think even "formalized mathematics" misses, is the fact that the computer can automatically verify correctness. At least for me, this is a big part of "the dream", i.e. that referees would no longer need to worry about whether something is correct, and could instead just focus on how interesting the math actually is.

[Rob Lewis]

I've been using "machine-checked mathematics" for a while, which I think is about the same as "computer verified" but can sometimes sound less off putting

[Rob Lewis]

A very minor point, Patrick, but I stumbled for a second over the word "completeness" in your intro paragraphs. "Completeness and consistency" sounds very much like you're talking logic, but you aren't, I guess you mean complete as in gap-free. Might be worth a few words to clarify this at the start

[Patrick Massot]

The main intended audience of made of people who, like me, have no idea about the technical meaning you're alluding to. But I'm open to adding a sentence if you can provide one.

[Kevin Buzzard]

Hey, I went to the 3rd year logic course, I remember what completeness means!

[Kevin Buzzard]

It either means that true things are provable, or provable things are true. Or something.

[Kevin Buzzard]

More seriously, I do think Rob has a point. Completeness and compactness and soundness are somehow the big theorems you learn when you're doing basic stuff like first order propositional calculus.

[Kyle Miller]

Maybe "thoroughness" or "exhaustiveness" could replace "completeness"?

[Rob Lewis]

Right, when you're talking about a syntactic proof system (like Lean) and put the words completeness and consistency next to each other, I read them as "the system can prove every semantic truth" and "the system can't prove false." I'm not saying you should write down these definitions, just that you should define what you mean by completeness to avoid the confusion.

[Arthur Paulino]

Am I too crazy to dream about a future in which humans will be doing mathematics with some ultra high tech interface that projects things in 3D and people will find and understand results by literally dragging and dropping pieces of a puzzle?

[Arthur Paulino]

:upside_down:

[Kevin Buzzard]

Some research level mathematics looks nothing like 3D objects.

[Mario Carneiro]

Most "visual programming languages" aren't really competitive with text input, so I'm dubious that this is actually the way of the future. The transhuman proof assistant interface probably looks more like vim :stuck_out_tongue:

[Arthur Paulino]

Ah, I didn't mean like the mathematical objects would be projected. I meant more the way Mario phrased it. But that's very true about current visual programming interfaces

[Yao Liu]

I thought completeness was fine, it's clear not about logic or real numbers. Consistency is more of a problem, imo. How about just correctness? And a word about being free of circular reasoning?
Formal mathematics does need a bit of rebanding...