Wiedijk's "Benchmark"

Stream: maths

[Kevin Buzzard]

In his 2007 paper "The QED Manifesto revisited" @Freek Wiedijk complains about how no prover at that time was suitable for formalising all of mathematics. I've said to Freek several times that I think Lean is a better candidate but he still moans about it for reasons I don't really understand. However one can look at the issues he raises which he says have not been solved, and then ask whether Lean solves them. For example he complains on p4 of the manuscript that none of the projects that existed at that time "have solved the difficult problem of how to integrate work by multiple people into a nice coherent whole". I think mathlib and github have solved that problem better than any of the systems he is talking about. He also highlights four mathematical statements and complains on the same page that none of the systems can "express all four statements in a good way". Statements are attached:

freek.png

How are we doing with that one? (2) and (3) I am completely happy that we can express naturally. How about (1) and (4)?

[Bhavik Mehta]

I want to say that (4) might be nicely expressible using the framework in the flypitch project: we could write the first-order logic sentence (in the language of set theory) expressing "2^{\aleph_0} = \aleph_2", and then just write essentially {ZFC + PFA} ⊢' that sentence

[Reid Barton]

I think the challenge in 4 is just to state the axiom PFA at all. I couldn't find a description of it that I could understand.

[Reid Barton]

We definitely can already formulate the conclusion $2^{\aleph_0} = \aleph_2$--it seems this is what the author was mainly concerned about.

[Reid Barton]

It's

import set_theory.ordinal

open cardinal

#check ((2 : cardinal.{0}) ^ omega.{0} = aleph 2)

[Reid Barton]

I was hoping PFA was some obscure statement about infinite combinatorics but it seems to really be an obscure statement about set-theoretic forcing

[Reid Barton]

or more precisely, it involves quantifying over all the formulas of the language of set theory

[Bhavik Mehta]

I don't see the difficulty there - once we have the basic definitions of forcing at least. Defining a stationary subset (see eg Def 8.1 of Jech Set Theory) of a regular uncountable cardinal is easy (and defining a regular uncountable cardinal should be easy if it's not already done), then given a forcing P we can define the generic model - from here we can easily define what a proper forcing is (I'm using Def 31.1 of Jech), and then PFA is easy (density and such are one liners). In particular I don't think we ever need to quantify over all formulas in the language of set theory, this is the sort of thing the forcing theorem and generic model theorem should fix nicely

[Bhavik Mehta]

I might be missing some subtlety though

[Reid Barton]

The difficulty is I don't know what forcing is.

[Reid Barton]

Wait, maybe not. Maybe you found a different formulation of the axiom than the ones I found.

[Bhavik Mehta]

I'm using the one on wikipedia and the one in Jech Set Theory

[Patrick Stevens]

Reid Barton said:

The difficulty is I don't know what forcing is.

I should warn you that forcing is an unsolved problem in exposition - although the best I've read so far is https://arxiv.org/abs/0712.1320

[Bhavik Mehta]

In any case, hasn't the flypitch project shown that lean can definitely define cohen forcing

[Kevin Buzzard]

Maybe but I doubt it can be used to say anything about the cardinals in data.cardinal

[Kevin Buzzard]

(or wherever they are, sorry)

[Bhavik Mehta]

Yeah I agree with that, I think the sensible way to formulate (4) would be defining cardinals in the language of set theory using the definitions from flypitch rather than set_theory.ordinal cardinals

[Gabriel Ebner]

Note that flypitch only defines a very limited class of forcing models. Essentially just Setᵤ and Setᵤ[G] (where Setᵤ is the collection of sets with cardinality less than Type u as defined in Lean).
But even with that you can still define properᵤ (i.e., proper in Setᵤ) and PFUᵤ. From there you should be able to prove that PFU₀ → Setᵤ ⊧ 2^ℵ₀ = ℵ₂ and I believe this should be equivalent to 2^ℵ₀ = ℵ₂

[Gabriel Ebner]

I believe the ordinals and cardinals in Setᵤ and Type (u+1) are isomorphic.