Does proof checking use theorems?

Stream: general

[Tim Daly]

DeMillo, Lipton, and Perlis (Social Processes and Proofs of Theorems and Programs) seem to believe that a proof checker has to grind a proof all-the-way-down every time. That is, the proof checker cannot assume that axioms hold and that every axiom needs to be re-proven as it is used. Is this how the lean proof checker works? Or does it 'believe' an axiom?

[Reid Barton]

Axioms are not proven at all. That's what makes them axioms.
Do you have in mind lemmas? Of course Lean does not re-check the proof of a lemma every time it is applied.

[Tim Daly]

I thought that was the case but, since I'm writing that refutation, I thought I'd 'fact check' it. Thanks.

[Jason Rute]

Here is the paper. https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf

[Tim Daly]

Fetzer (Program Verification: The Very Idea) seems to claim that algorithms are appropriate subjects for verification but programs are not. This seems to me to undercut the idea that 'programs are proofs'.

[Kevin Buzzard]

Programs aren't the same as proofs. Programs are a certain kind of proof. Lean is quite happy with proofs that aren't programs. Mathematicians use the word proof to mean something more general than a program

[Simon Cruanes]

The whole point of lean4 is that more of the prover is in lean itself, but using meta, right? So that's a lot of programs that are definitely not proofs.

[Tim Daly]

I agree that proofs are not (or need not be) programs. But "programs are proofs" is stated quite plainly in a whole stack of books on my desk. Fetzer seems to disagree.

[Simon Cruanes]

A very restricted subset of programs, with rich types, functions that are total, and no effects, may be considered as proofs of their type being inhabited. 99.99% of actual programs people write and execute are not proofs :upside_down:

[Jason Rute]

The second paper: http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf

[Jason Rute]

Also I couldn’t, with a very quick glance, find anything in the first paper about axioms having to be proven. Where do they say that?

[Tim Daly]

The view that everything needs to be re-proven seems (to me) to be implicit in their argument against verification. Social processes allow "proofs" to hand-wave the assertion that "we could prove it down to the metal if we wanted". They argue that verifications will involve dozens of pages. A verification of the GCD algorithm, if everything is expanded in all its glory (i.e. reproven) might take several pages but mathematical proofs rest on prior proofs, making them shorter, so I don't see that their objection is reasonable.

[Tim Daly]

Indeed, Dijkstra hand-proved a lot of his programs. His reply to DeMillo et al. is (A Political Pamphlet from the Middle Ages) (https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD638.html)

[Tim Daly]

Given that (some) programs are proofs, is there an example of a program that gets accepted by Lean?

[Gabriel Ebner]

The whole point of lean4 is that more of the prover is in lean itself, but using meta, right?

AFAIU meta is gone in lean4. However many interesting parts are implemented using an FFI to C++ code, and for those functions that are imported from C++ you can only prove that they produce some result value, but not which one.

[Tim Daly]

Martin-Lof's paper (Constructive Mathematics and Computer Programming) (https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf) claims "it no longer seems possible to distinguish the discipline of programming from constructive mathematics". Bob Harper uses it as the basis of his 2018 Oregon Lecture (https://www.youtube.com/playlist?list=PL0DsGHMPLUWXXA8RHzVZ2B5E5hP8CD15Z) (aside: Harper's courses are exceptionally good)

It seems, as far as I can tell, the "transition paper" from the prior discussion to a formal basis for program verification in Lean. (I read it before but not with this question "before the court").

[Chris B]

They argue that verifications will involve dozens of pages. A verification of the GCD algorithm, if everything is expanded in all its glory (i.e. reproven) might take several pages but mathematical proofs rest on prior proofs, making them shorter, so I don't see that their objection is reasonable.

Even the kernel makes use abstraction IE "theorem_x : T := h1 h2 h3 type-checks, so don't bother re-checking it at subsequent use sites". It's definitely the case that internally, Lean produces more data than a human would want to deal with in the process of convincing itself something is admissible, but isn't that why we're using computers in the first place?

As for an example of a program accepted by Lean, some minimal examples would be like the read/write registers that are used as a state_t tutorial in "Programming in Lean". Even just array access in lean using fin is a very cool example of a tiny program with a built-in spec that ensures all accesses are in-bounds . Off the top of my head I can't think of any good examples that aren't meta, but a lot of those could probably be un-meta'd just by giving them a gas parameter to ensure termination.

[Kevin Buzzard]

The thing is, it also no longer seems possible to suggest that constructive mathematics bears any resemblance to 99% of what actually goes on nowadays in mathematics departments.

[Chris B]

It takes all kinds brother. I say tomato, you say noncomputable example (tomato : Sort u) : nonempty tomato → tomato := classical.choice

[Tim Daly]

@Chris B funny :-)

[Tim Daly]

@Kevin Buzzard Lean is in the philosophy department (Avigaid is in both Philosophy and Math). The CMU CS department is heavily into types (Pfenning, Harper, Crary, Balzer, etc). I didn't see anyone from the Math department ( maybe my limitation). Computational Mathematics seems to be a hybrid discipline. Harper's book "Practical Foundations for Programming Languages" is certainly at the leading edge. I highly recommend it.

[Tim Daly]

@Kevin Buzzard One problem, not at all obvious to the Lean cohort, is the notation. A mathematician, on seeing a judgement, asked "what is that funny fraction?". It took me several courses and quite a while to be able to read papers containing whole pages of greek fractions with any understanding. The logic courses I took at CMU were all in the CS and Philosophy departments, not the math department. If you can read judgements then it doesn't seem to be a problem but if you can't it is a MAJOR barrier to understanding. And it is not an easy barrier to overcome.

[Johan Commelin]

Of course they do, and they shouldn't need to know it.

[Johan Commelin]

I personally would like "developing formal proof checkers" to be a subfield of math/CS that dies out as soon as possible.

[Tim Daly]

@Johan Commelin I've looked around at developing formal proof checkers and read some of the source code but felt lost. The closest published thing I've found was Paulson's "Designing a Theorem Prover" ( Abramsky, et al. "Handbook of Logic In Computer Science" Volume 2 Oxford Science Publications 1992 p415-475)

[Tim Daly]

Axiom has first class dependent types and insists on types EVERYWHERE. Those who know types find it painfully obvious. Those who don't find it obviously painful. It is a very steep learning curve. My mathematics background (covering results up to 1799) never mentioned types.

[Tim Daly]

Martin-Lof says "Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type"... that's not a phrase I think you'll hear in most math courses.

[Tim Daly]

I'm taking an algebraic topology course online and they have yet to mention the word 'type'.

[Johan Commelin]

Lot's of mathematicians have an intuitive understanding of types. Often, during a talk, someone will raise a question, asking "Where does $x$ live?". That's just asking for the type of $x$ in disguise. So that's not the problem. Most mathematicians are enthusiastic about dependent type theory when you explain it to them.
They have never formalised something.
People who know types find it obviously painful. Ask Mario. Ask anyone here who has met the "motive is not type correct" error.
That's why Mario is developing MM0 as a system that is not based on type theory.

[Johan Commelin]

So I would argue that you got it backwards. Most mathematicians find type theory "painfully obvious". Until they try it out in a theorem prover.

[Tim Daly]

Mathematicians find algebra painfully obvious until they try to use a computer algebra system, especially a strongly-typed system.

The type theory area is, like Lisp, an "enlightenment event"... you don't get it, you still don't get it, you wonder why ANYONE would get it, and then.... you wonder why anyone does anything else. Like Lisp, it is obviously correct you try to tell the next person... who doesn't get it.

I've bounced off Bishop's Foundation of Constructive Analysis book twice, despite Martin-Lof's recommendation.It's not the math I find hard, it's the change of mindset.

[Kevin Buzzard]

I have no idea about what those weird fractions mean and believe you me, you don't need to know if you're just interested in mathematics.

[Kevin Buzzard]

I have never had a clue about those fractions. That's why I can't read beyond page 2 of Mario's thesis.

[Kevin Buzzard]

But I am convinced it is of very little relevance to mathematics. He's just checking Lean works at some level beyond which I have lost interest.

[Kevin Buzzard]

Just like he might not care about talking to an engineer at Intel about how you get the wires on the chips

[Marc Huisinga]

lean's "logic and proof" discusses the notation: https://leanprover.github.io/logic_and_proof/propositional_logic.html

[Tim Daly]

This is a serious problem, though. It occurs in every area of math I've touched. I maintained a "computer algebra system" called Magnus, which is a special area called Infinite Group Theory. It took a long time to "come up to speed" on the notation, not to mention the concepts they represent, and then the dance one has to do to input math into a computer. Once you spend a year on it, you'll find that Infinite Group Theory isn't THAT hard and the notation and jargon "makes sense".

One of the key barriers, in my opinion, to wider adoption of computational mathematics is the "impedence mismatch" between what you know and what you have to type, that is, between your problem and your expression of your problem. It is quite a gap.

[Tim Daly]

@Marc Huisinga That all makes sense "in the small"... then you try to read "An Intuitionistic theory of types" by Martin-Lof and encounter pages 12 and 13. I'd be hard pressed to convince a mathematician that the +-elimination rule was "obvious".

[Tim Daly]

Computational Mathematics is almost a separate subject and a separate department of study.

[Tim Daly]

When I started in this game there wasn't a "computer science degree". You were a business major and they taught COBOL, an engineering major and learned FORTRAN, or a math major and learned LISP. I expect that within a generation there will be a "Computational Mathematics" department that is not Philosophy, Computer Science, or Mathematics.

[Marc Huisinga]

it's certainly often not easy to convince yourself that these rules are exactly the ones you want. in many cases, the theorems you prove about the rules are what provides the insight.
i'm not convinced that this is at all limited to computational mathematics, though; i'm sure one could dig up plenty of logic papers where this notation is used and it's also difficult to understand why the rules are what you want.
you might not even need the notation, i'm sure one could spend a while pondering about the zfc axioms :)

[Tim Daly]

One useful Computational Mathematics course would involve developing a stand-alone proof checker for a system like Lean.

[Mario Carneiro]

@Kevin Buzzard

I have never had a clue about those fractions. That's why I can't read beyond page 2 of Mario's thesis.
But I am convinced it is of very little relevance to mathematics. He's just checking Lean works at some level beyond which I have lost interest.
Just like he might not care about talking to an engineer at Intel about how you get the wires on the chips

I think this is the right idea. My work on lean's type theory, and MM0, are in the area of foundations of mathematics (or foundations of theorem provers if you prefer). It is not and should not be relevant for all mathematicians. The mark of a good foundation is that it stays in the background where you never have to see it. It is just there to answer questions in case you acquire some existential dread that nothing you are doing makes any sense.

In particular, for anyone that is wondering if MM0 would have any effect on their work: if you are doing math in lean, just keep doing what you are doing. Someday the whole foundation of lean might shift to something else, but it will be done in such a way that all the constructs built on top will be unaffected (modulo some engineering challenges that are my problem and not yours).

[Kevin Buzzard]

This is a serious problem, though. It occurs in every area of math I've touched. I maintained a "computer algebra system" called Magnus, which is a special area called Infinite Group Theory. It took a long time to "come up to speed" on the notation, not to mention the concepts they represent, and then the dance one has to do to input math into a computer. Once you spend a year on it, you'll find that Infinite Group Theory isn't THAT hard and the notation and jargon "makes sense".

One of the key barriers, in my opinion, to wider adoption of computational mathematics is the "impedence mismatch" between what you know and what you have to type, that is, between your problem and your expression of your problem. It is quite a gap.

Hales remarked in his talk in Pittsburgh last week that mathematical notation seems to fit very well with dependent type theory. Apparently we do know what we're doing, but just use exotic notation to express types for historical reasons.

[Tim Daly]

@Kevin Buzzard You've made a call for formalizing mathematics (in Lean). Tony Hoare (https://vimeo.com/39256698) has made another "Grand Challenge" call, which in my mind, also involves Lean. Hoare says his Grand Challenge is targeted at software engineering and the science of programming. The challenge consists in the construction, evaluation, and deployment of a high level programming language compiler, one that verifies the correctness of each program that it compiles. In my mind, Lean has a central role in his Grand Challenge.