A benchmark of four statements

Stream: general

[Johan Commelin]

In http://mizar.org/trybulec65/8.pdf, section 3, Freek Wiedijk gives four statements as small benchmark of how usable a proof assistent is for mathematicians. How does Lean fare here? My impression is that we don't have any trouble with (2) and (3). For (1), I don't think we currently have such a nice syntax for integrals and infinite sums, but we can probably get close. (4) is something that I don't know anything about.

[Joseph Tassarotti]

Coming from the Coq world, the issue he points out for Mizar with respect to 1 is indeed probably unlikely to be a problem, since it is not a problem in Coq. But the real subtlety (which I expect to happen also in Lean) is that the proof that consists of a chain of equalities like that in Coq wouldn't mean what Mathematicians usually think. In order for rewriting by a chain of equalities to be conveinient, it usually means setting things up so that it would say "if the integral exists, then it is equal to that", whereas most mathematicians would probably read that chain of arguments as a claim about the existence of the integral as well

[Joseph Tassarotti]

It's amusing to look at the 100 theorems table in that paper though. It doesn't even mention MetaMath, a lot has changed!

[Rob Lewis]

I think his concerns about classical reasoning in Coq are kind of misdirected. It's not so much a systems issue, but the big libraries aren't designed to support it. The mathcomp-analysis project is mostly (or entirely?) classical from what I understand. Given Mario, Jesse, and Floris' set theory work, I don't see why 4 should be an issue in theory. And it should be possible to do something analogous in Coq.

[Joseph Tassarotti]

I think his concerns about classical reasoning in Coq are kind of misdirected. It's not so much a systems issue, but the big libraries aren't designed to support it. The mathcomp-analysis project is mostly (or entirely?) classical from what I understand. Given Mario, Jesse, and Floris' set theory work, I don't see why 4 should be an issue in theory. And it should be possible to do something analogous in Coq.

Yeah, the 4 axioms he lists are basically sufficient in my experience :D. The real issue is that sociologically, many Coq people seem to strive to use as few such axioms as possible. (For example, the Coquelicot library that pre-dated mathcomp-analysis goes out of its way to use as weak of classical axioms as possible)

[Rob Lewis]

It's amusing to look at the 100 theorems table in that paper though. It doesn't even mention MetaMath, a lot has changed!

On the other hand, it's always fun to look back at some of the Automath literature and see how little has changed. https://pure.tue.nl/ws/files/2039924/256169.pdf

[Rob Lewis]

(Also https://www.win.tue.nl/automath/about_automath/mkm-compleet-klein.pdf, one of my favorites.)

[Rob Lewis]

Yeah, the 4 axioms he lists are basically sufficient in my experience :D. The real issue is that sociologically, many Coq people seem to strive to use as few such axioms as possible. (For example, the Coquelicot library that pre-dated mathcomp-analysis goes out of its way to use as weak of classical axioms as possible)

Indeed, which means he has a fine answer for why Coq didn't fulfill the QED vision, but not for why it couldn't. Which I think is more what he was trying to argue.

[Jesse Michael Han]

#4 is probably doable at the level of Lean's set theory. going 1 level deeper and showing that exactly ZFC + PFA negates CH would be a lot of work, but as Rob says, doable in theory.

[Kevin Buzzard]

(Also https://www.win.tue.nl/automath/about_automath/mkm-compleet-klein.pdf, one of my favorites.)

What do people make of p32? :-)

[Jesse Michael Han]

oh nevermind my first claim, it's an open problem whether one can even define forcing extensions at the level of Lean's set theory

[Johan Commelin]

p9 and p10 seem to reflect some of the mm0 design decisions, I think

[Johan Commelin]

@Rob Lewis Thanks for that link, it's interesting, and I didn't know about it

[Jesse Michael Han]

some of Automath's "important decisions" seem to reflect mm0 design decisions also:

Don't try Automatic Theorem Proving

Prefer the use of TYPED SETS, but don't forbid untyped sets

Don't put logic in the system; let the user start his books with it.

Don't put induction and recursion in the system; consider it as book material, even when that might be slightly clumsier.

[Johan Commelin]

Exactly

[Johan Commelin]

@Kevin Buzzard I have no idea how to interpret p32

[Rob Lewis]

What do people make of p32? :-)

I stuck that picture at the end of my dissertation. Personally I'm more partial to p7 though, that one went at the front.

[Rob Lewis]

Rob Lewis Thanks for that link, it's interesting, and I didn't know about it

There's a lot of interesting stuff here: https://www.win.tue.nl/automath/

[Andrew Ashworth]

I had no idea de bruijn's phd was in number theory before he became a very famous big deal computer scientist

[Andrew Ashworth]

well, maybe not? I actually have no idea when computer science split off from logic and math

[Johan Commelin]

Yeah, and now Kevin is trying to imitate him (-;

[Johan Commelin]

Fun fact: Gijswijt was awarded the N.G. De Bruijn prize for his work on the cap set problem.

[Johan Commelin]

That theorem was recently formalised by Dahmen, Hölzl, and Lewis.

[François G. Dorais]

@Jesse Michael Han PFA doesn't mention forcing extensions, it's just another set theoretic axiom. That said, we're a long way from formulating the definition of a proper forcing, so #4 is only theoretically possible.

[Jesse Michael Han]

what's your definition of a proper forcing?

[François G. Dorais]

There are several equivalent definitions, some of which are more closer to reach, but these are not the ones that are useful in proving that the relevant forcings for #4 are proper. Closer to reach is that Martin's Axiom for forcings of size Aleph_1 implies the negation of CH since the ccc is straight forward to define and the relevant proof of ccc mostly involves just one combinatorial trick.

https://en.wikipedia.org/wiki/Proper_forcing_axiom

[François G. Dorais]

I just read that Wikipedia article and I see that they only give one definition. The definition given there is most useful to prove that forcings are not proper. The most versatile one is perhaps the existence of master conditions, as detailed in Uri Abraham's handbook article IIRC. Shelah has a slick game theoretic definition that one could probably write down in Lean pretty quickly, but that definition is mostly a curiosity.

[Jesse Michael Han]

right, MA is easy to shallowly state in Lean, but i made my earlier claim because it's not clear to me how one would state "proper forcing" for a partially ordered type; the rest of PFA is fine.

in principle, if we had the ZFC proof tree for "PFA implies not CH" we could replay it in Lean's canonical model pSet of ZFC and then use the fact that Lean's (external) cardinals are isomorphic to pSet's cardinals to conclude "if PFA holds in Lean's canonical model of ZFC, then CH is false for Lean's cardinals"

but this is different from an intrinsic statement of PFA in Lean

ah i see you beat me to the punch. if there's a definition of "proper forcing" which avoids an implicit quantification over forcing extensions then that should be fine.

[François G. Dorais]

There is never any need to quantity over forcing extensions, all of that can be done in the forcing language, which is in the ground model.

[Jesse Michael Han]

i thought you might say that :P

it's not really clear to me what the right definition of the forcing language of a partially ordered type is

there's the bSet construction which gives you a proper class of P-names, but then one is essentially working with a forcing extension

[François G. Dorais]

The P-names are ground model sets, so they're not a problem. The tough part is defining the forcing language, specifically the atomic relations for membership and equality, which is traditionally done as a mutual transfinite recursion.

[Jesse Michael Han]

if we replace P with a boolean completion B, i think constructing the forcing language is tantamount to exhibiting the B-valued L_ZFC structure on the B-names, which we know how to do (here P and B are types)

still, this seems to give a rather unpleasant definition of PFA. is there a definition of "proper forcing" which avoids P-names entirely?

[François G. Dorais]

Yes there is. But, side issue, the proof of the consistency of not CH in Lean that I read some while ago actually falls short of Cohen's actual theorem since it only shows that Lean (+AC) proves Con(ZFC+not CH). The piece that is missing is the internal definition of the forcing language, which shows that ZFC itself proves that Con(ZFC) implies Con(ZFC+not CH).

[Jesse Michael Han]

yes, we intentionally avoided working internally as much as possible (formal proofs get an order of magnitude slower working in an embedded logic)

the project is aptly named "a formal proof of the independence of the continuum hypothesis", not "a formal proof that there is a formal proof of the independence of the continuum hypothesis from ZFC, in ZFC" :^)

getting from Lean +(AC) proves Con(ZFC + not CH) to Lean +(AC) proves (ZFC proves Con(ZFC) implies Con(ZFC + notCH)) is definitely an open problem though. i don't think it's doable with the current state of the art, and it would be very interesting to see how to get there.

[François G. Dorais]

You don't need an embedded logic, all you need is to avoid increasing type levels. Concretely, the membership and equality relation for Type n names doesn't need Type n + 1. Once that's done, you have Cohen's actual theorem, mod some typical meta translations.

[François G. Dorais]

(The "mod" part actually involves a major part of Mario's thesis, so "typical" was perhaps a strong word there.)

[Jesse Michael Han]

you need an embedded logic (ZFC) to even state the result, let alone formally prove it

you would also need to formalize those parts of Mario's thesis, which are about Lean and ZFC, in Lean

to be clear, when i say "open problem", i mean "open formalization problem"

[François G. Dorais]

No, I don't think that's true at all. All you need is the idea of nice names so that names don't need to be "proper classes", up to equivalence. This is a key idea in Solovay' s model where all sets of real are Lebesgue measurable, and also a beta-step to much later set theory.

[Mario Carneiro]

It is difficult to do developments in lean "avoiding Type 2" with any reasonable confidence that you've done so

[Mario Carneiro]

it's not like lean tracks universe levels in its "axioms" list

[Mario Carneiro]

My thesis isn't very precise about the particulars of how many universes entail how many inaccessibles and vice versa because getting the optimal result requires a lot more care and some "large" constructions (i.e. proper class things and universes that you can only kind of talk about in lean)

[Mario Carneiro]

What do people make of p32? :-)

I think it is not incorrect to say that mathematics is not formalized until it is already "dead"; certainly I have only ever had experience with dead math in theorem provers. The only part of that slide I would correct is that formalization requires a "competent mathematician", not a "beginner + computer". In order to formalize a thing you have to already understand it at a pretty deep level, because you will be asked to fill in all the details. A beginner + computer setup is however sufficient for verifying a formal development.

[Mario Carneiro]

In http://mizar.org/trybulec65/8.pdf, section 3, Freek Wiedijk gives four statements as small benchmark of how usable a proof assistent is for mathematicians. How does Lean fare here?

More generally, I think lean fares very well on almost every point in the paper, from the technical aspects (classical mathematics, set theory, dependent types, ...) to the social aspects (many contributors and well organized). But there is one part that worries me:

Ideally, the system should be set up in such a way, that the mathematics that is formalized in it can survive a ‘redesign of the foundations’. Suppose that one builds a QED-like library on top of Coq, and then changes one’s mind and switches to a HOL-like system. Basically, this will mean that one will have to start from scratch. It seems very arrogant to think that we already know what the best foundations for our formal library should be, and one would therefore prefer not to be ‘locked in’ to a specific version of the foundations.

I think lean has a serious problem with "lock-in". The proof scripts in mathlib are all tied pretty tightly to the lean 3 setup, and lean 3 is a monolithic checker with no alternate implementations and no spec. Moreover, lean has already been through an upheaval once, from lean 2 -> lean 3, and the library did not survive (to a first approximation). I think Lean dodged a bullet when it comes to foundational complexity - the situation is not optimal but at least soundness is not an open question.

To me, the dream system is a Lean frontend on an MM0 backend. That's as close to perfect on all these points as I can currently envision.

[Johan Commelin]

@Mario Carneiro So let's build that frontend!

[Johan Commelin]

I would be willing to devote a serious amount of time on such an effort

[Johan Commelin]

But first I need breakfast :grinning:

[François G. Dorais]

It is difficult to do developments in lean "avoiding Type 2" with any reasonable confidence that you've done so

It's been a while since I looked at flypitch, perhaps I should look again, but the issue wasn't "avoiding Type 2" but that the result of the construction wasn't at the same level. I didn't see at the time how one could get a proof in Lean+AC that Con(Lean+AC) implies Con(Lean+AC+not CH) using flypitch the same way Cohen did for ZFC. However, I did think that it should be possible to rework the Boolean valued interpretation at the same level and that could possibly be used to give an interpretation of Lean+AC+not CH in Lean+AC, and therefore the relative consistency result.

[Giovanni Mascellani]

I think lean has a serious problem with "lock-in".

I completely agree with your idea about separating the untrusted and complex frontend from the trusted and simple backend, but I think the paragraph you quote mentions a different lock-in, i.e., the decoupling of the "higher level" library from the logic foundations. Usually "real mathematicians" do not state their logic foundations in their work or talks; most of them do not even know much about it, except some vague ideas of set theory. Everybody assumes there is an informally stated but mostly agreed-upon common level where you can take functions, sets, numbers and some other objects and manipulate as we are used to. And then logicians are supposed to know how this common level is encoded in term of everyone's favourite foundational theory.

I think that what Wiedijk envisions in that paragraph is the identification and formal definition of this common level, and the encoding of a higher level library exclusively in terms of this level, so that the logical foundation below can be swapped at one's desire without touching the upper part.

I don't think I know any system organized in this way. In each system the artifacts of the underlying theory are visible at each level, and sometimes they are actively sought after, like all the advanced tricks with dependent types in Coq (and possibly in Lean too, but I do not know much beside very basic Lean).

Metamath tries to avoid relying too much on how objects are encoded in terms of sets, but there is no watertight separation (there are some efforts, like the extensible structures logic). If the separation was watertight, most of the humour section would not be possible.

[Johan Commelin]

Back to p32, on the lifecycle of a mathematical concept... (aka, mathematics is dead once it's formalised). Does that mean that Kevin, Patrick and I were the undertakers that buried the last remains of perfectoid spaces?

Perfectoid space (2011 – 2019†). R.I.P.

[Kevin Buzzard]

I think that the slide has dated a lot. I think if computers understand mathematics then they will be able to help us to do it in ways that de Bruijn had not imagined.

[Simon Hudon]

Addendum: if mathematicians understand formalized mathematics, they can start learning from the proof techniques that are being used

[Reid Barton]

Used where?

[Reid Barton]

It would be more useful to learn, say, Russian

[Simon Hudon]

... being used in formal proofs. The objection that formalizing a subject kills it is not surprising when we think that a lot of mathematicians don't want to learn the language. If they knew the language of formal mathematics, it's reasonable to expect that the story would be very different

[Kevin Buzzard]

It is still the case that mathematicians can get a lot more out of an informal pdf (even one with mistakes) than an undocumented formal proof -- or at least they can get more out more quickly. Even a mathematician who can understand the Lean code. That's why we need heavily documented code.

[Simon Hudon]

"we need heavily documented code" is still a different claim than "mathematicians can't learn anything useful from a formal proof"

[Kevin Buzzard]

That's true, but I think it's also true that a well-written pdf teaches you much more efficiently than a formal proof and no amount of learning about what a formal proof is will fix this. I think mathematicians communicate mathematics at a far higher level than formalised code, by which I mean really far far higher than you might think as a computer scientist. We talk in analogies and wave our hands and draw pictures and are actually communicating sketch proofs of completely rigorous arguments which we all know are formalisable but which we would never bother to formalise.

[Reid Barton]

My point is that, at least currently, basically all formal proofs are "translations" of proofs which are already available in informal form, so there is no need to understand the formalized proof--one can just read the informal one.