Zulip Chat Archive

Stream: maths

Topic: Why formalize mathematics


Patrick Massot (Dec 05 2021 at 13:30):

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 (Dec 05 2021 at 13:33):

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 (Dec 05 2021 at 13:44):

(deleted)

Eric Taucher (Dec 05 2021 at 14:04):

cognitive dissonance One of my favorite phrases. :grinning:

Johan Commelin (Dec 05 2021 at 16:25):

@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 (Dec 05 2021 at 16:57):

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

Patrick Massot (Dec 05 2021 at 17:11):

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

Patrick Massot (Dec 05 2021 at 17:11):

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

Scott Morrison (Dec 05 2021 at 19:29):

In the abstract: s/loosing/losing/.

Scott Morrison (Dec 05 2021 at 19:32):

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 (Dec 05 2021 at 19:33):

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 (Dec 05 2021 at 19:34):

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 (Dec 05 2021 at 19:36):

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 (Dec 05 2021 at 19:50):

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 (Dec 05 2021 at 19:51):

Last sentence of abstract: s/apply/applies/

Yury G. Kudryashov (Dec 05 2021 at 19:55):

Computer readable mathematics?

Adam Topaz (Dec 05 2021 at 19:57):

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

Patrick Massot (Dec 05 2021 at 20:17):

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 (Dec 05 2021 at 20:18):

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 (Dec 05 2021 at 20:21):

Maybe "computer reasoned mathematics"?

Kevin Buzzard (Dec 05 2021 at 20:23):

21st century mathematics ;-)

Arthur Paulino (Dec 05 2021 at 20:26):

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

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

Jeremy Avigad (Dec 05 2021 at 20:37):

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 (Dec 05 2021 at 20:46):

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 (Dec 05 2021 at 20:49):

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 (Dec 05 2021 at 20:54):

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 (Dec 05 2021 at 21:24):

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

Patrick Massot (Dec 05 2021 at 21:30):

This whole business is all about anticipating our bright future.

Adam Topaz (Dec 05 2021 at 21:46):

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 (Dec 05 2021 at 23:17):

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 (Dec 05 2021 at 23:20):

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 (Dec 05 2021 at 23:47):

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 (Dec 05 2021 at 23:48):

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

Kevin Buzzard (Dec 05 2021 at 23:48):

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

Kevin Buzzard (Dec 05 2021 at 23:52):

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 (Dec 06 2021 at 00:15):

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

Rob Lewis (Dec 06 2021 at 00:16):

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 (Dec 06 2021 at 22:18):

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 (Dec 06 2021 at 22:19):

:upside_down:

Kevin Buzzard (Dec 06 2021 at 22:42):

Some research level mathematics looks nothing like 3D objects.

Mario Carneiro (Dec 06 2021 at 22:42):

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 (Dec 06 2021 at 22:45):

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 (Dec 07 2021 at 09:18):

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...


Last updated: Dec 20 2023 at 11:08 UTC