Flyspecking Flyspeck

Stream: lean4

[Timothy Chow]

My main takeaway from Flyspecking Flyspeck by Mark Adams is that it's important, for auditing purposes, to be able to export a proof object file and validate that file using a separate piece of software. Is this a capability that Lean 4 has? If so, are there step-by-step instructions somewhere, explaining how to do this?

It seems to me that even this kind of "independent" check might not be completely independent. For example, it would certainly be tempting to use the same version of GMP during the audit as during the original proof. What other libraries besides GMP might one worry about?

On a slightly different but related note, suppose I formulate and prove a theorem, and I carefully check all the definitions in mathlib that I'm relying on, to convince myself that they mean what I think they mean. Suppose that I worry that mathlib might evolve in such a way that my theorem is still correct, but no longer proves exactly what I think it proves. Is there a mechanism by which I can "lock in" a particular version of mathlib (or the relevant portions of mathlib) along with my theorem, to preclude this kind of "definition drift"? More generally, what community standards are in place to minimize the possibility of definition drift in mathlib?

[Henrik Böving]

You can extract with: https://github.com/leanprover/lean4export and feed it to third party kernels (or indeed also the kernel itself again), such as https://github.com/ammkrn/nanoda_lib

[Floris van Doorn]

More information about (external) type checking can be found here: https://ammkrn.github.io/type_checking_in_lean4/

[Floris van Doorn]

Definition drift is a potential issue, since definitions do get changed in Mathlib. The review cycle and Mathlib standards will usually ensure that a definition doesn't just change to a mathematically meaningfully different definition, but in edge cases this could be a problem.

That said: every Lean project completely specifies which version of Mathlib it is built with, and (unless you update it), it will stay on that Mathlib version.

[Timothy Chow]

Here's a related question. How often does it happen that a proof that works perfectly fine with one version of mathlib breaks with a newer version of mathlib? I can think of various reasons why this might happen. Definitions might be eliminated entirely, or at least changed materially. It could also be that powerful tactics such as grind don't increase in power monotonically, but stop being able to prove things that they used to be able to prove.

Does this sort of thing happen much in practice? Are there other reasons why a proof might break when mathlib is upgraded?

[Ruben Van de Velde]

Very common, yes

[Chris Henson]

If you filter for commits bumping the Lean toolchain and/or look at things marked with #adaptation_note these are not too hard to track down.

[Ruben Van de Velde]

Things getting renamed are common, for example

[Ruben Van de Velde]

Files being moved around, tactics changing (typically becoming stronger)

[Chris Henson]

Oh I misunderstood, I was talking about changes in Lean itself. A different issue, but still somewhat relevant.

[Ruben Van de Velde]

New linters, if you have those turned on

[Ruben Van de Velde]

Hypotheses being weakened, as well

[Timothy Chow]

Can a tactic becoming stronger cause a proof to break? It didn't occur to me that that could happen, but maybe it could?

[Ruben Van de Velde]

Well yes, for example if it finishes the proof earlier, you get a "no goals to be solved" error. A more complex case that I hit recently was with field_simp gaining support for inequalities, where the rest of the proof assumed it didn't

[Kevin Buzzard]

Timothy Chow said:

Here's a related question. How often does it happen that a proof that works perfectly fine with one version of mathlib breaks with a newer version of mathlib?

Click on a few of these PRs (bumps to mathlib in the FLT project) to see things going wrong:
https://github.com/ImperialCollegeLondon/FLT/pulls?q=is%3Apr+is%3Aclosed+bump . Ignore the changes to system files (these are typically at the bottom) but observe that there's just general noise as things get upstreamed (e.g. someone defines X or proves X and dumps it in FLT, and then someone moves it up to mathlib and during the process the name changes and/or the order of, or number of, inputs changes, and then things break). More complicated to fix are when the behaviour of simp changes.

[Ruben Van de Velde]

Yeah, though issues with upstreaming code tend to only happen if you (or one of your contributors) actively make them happen