The original article is about a potential mathematical revolution, where computer verified proof has gone mainstream. The stuff about using weaker axiom systems, or getting theorems without needing AC is interesting, but I'd argue it is not so relevant. More important are things like this:
"The thing that’s so remarkable about this new foundation is that the fundamental concepts are much closer to where ordinary mathematicians do their work. In the usual foundation, Zermelo-Frankel set theory, it takes an enormous amount of work just to build up the basic concepts and theorems that mathematicians rely on every day. The result is that if you want a computer to check your proofs, you have to teach it all that theory first. Essentially, you have to give it the same education you got — except that you have to do it in a far more exacting way. As a result, the only people so far who have used computer proof systems are computer scientists who specialize in it, and it takes them many years of effort to check a single new theorem. Georges Gonthier, for example, spent a decade checking the four-color theorem.
But this approach circumvents all that labor. Not only that, but the language the computer understands is far closer to natural mathematical language."
I should point out that the Four-Colour Theorem was formalised in Coq, not a ZF-based proof assistant. But that aside, these are pretty big claims. I'd like to hear what sort of basic theory is being talked about, and how the proofs are closer to natural language. On the stackexchange thread, ek comments:
"Anyone who has used Coq will tell you that the proofs that you produce often don't end up looking much like equivalent plain-English proofs at all."
But this doesn't strike me as fair. I'm a HOL Light user, and the de facto proof style is procedural. In that style, which I understand is preferred also in Coq, the user tells the machine how to compose an assortment of automated tools to break down and solve the problem, often performing computations to massage the goal into a suitable form. The scripts are usually completely unreadable, but that's by design. Those who want a more readable style of formalised proof are encouraged to use "declarative styles".
How do the claims made about HoTT's readability factor in here?
>But this doesn't strike me as fair. I'm a HOL Light user, and the de facto proof style is procedural. In that style, which I understand is preferred also in Coq, the user tells the machine how to compose an assortment of automated tools to break down and solve the problem, often performing computations to massage the goal into a suitable form. The scripts are usually completely unreadable, but that's by design. Those who want a more readable style of formalised proof are encouraged to use "declarative styles".
It's possible to create readable coq scripts. However, like with any kind of programming it takes effort. If you take a look at the proof of four colors theorem of fiet thompson they are quite readable and don't look like complete mess. They, however, use modified coq instead which is called ssreflect.
"The thing that’s so remarkable about this new foundation is that the fundamental concepts are much closer to where ordinary mathematicians do their work. In the usual foundation, Zermelo-Frankel set theory, it takes an enormous amount of work just to build up the basic concepts and theorems that mathematicians rely on every day. The result is that if you want a computer to check your proofs, you have to teach it all that theory first. Essentially, you have to give it the same education you got — except that you have to do it in a far more exacting way. As a result, the only people so far who have used computer proof systems are computer scientists who specialize in it, and it takes them many years of effort to check a single new theorem. Georges Gonthier, for example, spent a decade checking the four-color theorem.
But this approach circumvents all that labor. Not only that, but the language the computer understands is far closer to natural mathematical language."
I should point out that the Four-Colour Theorem was formalised in Coq, not a ZF-based proof assistant. But that aside, these are pretty big claims. I'd like to hear what sort of basic theory is being talked about, and how the proofs are closer to natural language. On the stackexchange thread, ek comments:
"Anyone who has used Coq will tell you that the proofs that you produce often don't end up looking much like equivalent plain-English proofs at all."
But this doesn't strike me as fair. I'm a HOL Light user, and the de facto proof style is procedural. In that style, which I understand is preferred also in Coq, the user tells the machine how to compose an assortment of automated tools to break down and solve the problem, often performing computations to massage the goal into a suitable form. The scripts are usually completely unreadable, but that's by design. Those who want a more readable style of formalised proof are encouraged to use "declarative styles".
How do the claims made about HoTT's readability factor in here?