[FOM] Improving Set Theory

[Timothy Y. Chow]

Harvey Friedman wrote:

> I gather from some comments I have seen that there is a bit of a crisis, 
> with regard to Proof Assistants aimed at creating formal proofs.
>
> The fact that it can be done with some practicality for big deep
> theorems was an impressive achievement. There seems to be some
> skepticism that one can get together the resources necessary to do it
> for the biggest deepest theorems - being hard to argue on the basis of
> need and major consequence. (I am distinguishing this from Proof
> Assistance aimed at verifying the correctness of engineering systems).

I'd be curious to hear more about this alleged "crisis."

There are various possible obstacles to scaling up from the current 
situation to a situation where all or most of mathematics is routinely 
formalized.

For example, there are sociological obstacles that have next to nothing to 
do with the technical merits of proof assistants.  There is very little 
reward, in terms of jobs, awards, and promotions, for learning how to use 
a proof assistant and formalizing proofs of one's own theorems in them. 
Also, the existing documentation is still poor, at least from the point of 
view of a mathematician.

Another possible obstacle, which sounds like what Harvey is talking about, 
is the existence of specific theorems or bodies of knowledge that present 
technical obstacles for existing proof assistants.  I've heard a little 
bit about such things, but not too much, and what I've heard does not 
suggest that types are the problem and we should switch to sets.  If some 
people are saying that, I'd like to hear more details.

Below, I quote (with permission) some remarks by Kevin Buzzard about where 
things currently stand, from his perspective as a number theorist who has 
only recently jumped into the proof assistant game.  For context, I was 
asking him why he was proposing Lean as opposed to Coq or HOL or something 
else.

I believe that Jeremy Avigad has been involved with Lean so I would be 
particularly interested to hear his perspective.

Tim

> Two problems with Coq: (1) it really wants you to do constructive 
> mathematics, and (2) it doesn't have quotients. If you have an 
> equivalence relation on a type (i.e. a set) and you want to construct 
> the set of equivalence classes plus the universal property, you're out 
> of luck. You have to work with the big object and consider functions on 
> it which are constant on equivalence classes. They even have a word for 
> it -- "setoid hell". Lean does not have this problem. For me, Lean is 
> the only one worth learning if you actually want to do mathematics. The 
> simple type theory ones like HOL Light can't do dependent types, which 
> means in practice that they can't do presheaves of rings on a 
> topological space, which means that they can't do schemes (or perfectoid 
> spaces). Coq has no quotients and the HoTT systems simply don't have any 
> mathematics in them. Nothing at all, it seems to me, apart from the 
> basic definitions: groups, rings, fields, the real numbers, the p-adic 
> numbers for some reason, and then a load of stuff about categories. And 
> real problems with the axiom of choice. Lean lets you use the axiom of 
> choice without any fuss, and the law of the excluded middle.
> 
> Here is what Lean currently knows about:
> 
> https://xenaproject.wordpress.com/what-maths-is-in-lean/
> 
> It is no joke to say that this is a far better approximation to an 
> undergraduate maths curriculum than any of the other systems have, and 
> it is progressing through MSc and harder mathematics extremely rapidly. 
> Sure Coq has a proof of the four colour theorem and the odd order 
> theorem, but everything is spread around in different libraries. We have 
> everything in one library in Lean. The HOL systems can only take you so 
> far because simple type theory does not seem to me to be strong enough 
> to do modern mathematics in a convenient way, although note that 
> Isabelle/HOL and perhaps other HOL systems have a healthy amount of 19th 
> century analysis (e.g. Dirichlet's proof of infinitely many primes in an 
> AP). Lean has that too, but we cheated; we stole the proof from metamath 
> via a computer program which can translate certain proofs from one 
> language to another under highly favourable circumstances.
> 
> I feel like someone trying to persuade a neutral to support their own 
> football team, but as a mathematician who has taken the time to have a 
> good look at all the systems, I have come to the same conclusion as 
> Hales: Lean is currently our best bet. This might not always be the case 
> but in 2019 I think it is.