djb's formalization of McEliece

Stream: general

[Henrik Böving]

djb (A very popular crypto, as in encryption, not as in crypto currency person) seems to be working towards formally verifying McEliece (a quantum computer resistant asymmetrical encryption scheme) in Lean 4!: https://mastodon.cr.yp.to/@djb/110780690497105946

[Eric Rodriguez]

I'm fairly sure he's in the zulip :]

[Matthew Ballard]

Beware that Lean is a general-purpose programming language. Malicious code anywhere inside the Lean software or inside leangoppa can spoil verification, destroy files, etc. In other words, the proof verification relies on a large TCB.

[Ruben Van de Velde]

Is there an independent verifier for lean4 yet?

[Henrik Böving]

I don't think djb is alluding to the kernel (aka the verifier) here, I'm rather certain he would agree that that is a very small TCB. I would guess the comment is directed more towards the fact that in the end you have to also trust that the compiler makes a faithful translation of your statement and proofs for the kernel to look at. And having an independent second Lean compiler is kind of pointless because the meta programming relies heavily on knowing precise internal things about the compiler

[Henrik Böving]

Now if you listen to e.g. Leo's talks you will notice that he says only the kernel is TCB and the compiler does not need to be trusted which is a fair statement to make in the sense that it is unlikely that the compiler will wrongly translate your statement and then still allow the proof that you wrote for the actual statement to go through. But technically speaking you still trust.

[Kevin Buzzard]

Yes Dan was at Leiden two weeks ago and has been active in discussions about this work in the private stream associated to the workshop

[Frédéric Dupuis]

I'm pretty sure "trusted" here mainly means "trusted not to install a keylogger on your machine".

[Jireh Loreaux]

I would have thought "trusted" meant something more like Ken Thompson's "Reflections on trusting trust".

[Wojciech Nawrocki]

Oh, hey, @Joe Hendrix and I did some work on McEliece as well :) On a cursory look, djb's repo seems to be aiming at verifying the mathematics of Goppa codes and eventually McEliece. In lean-crypto, we were looking at the mostly orthogonal target of showing a concrete C implementation equivalent to a reference implementation in Lean 4.

[Johan Commelin]

@D. J. Bernstein You might be interested in chiming in on this thread :this:

[Jason Rute]

Just so it is clear, it is entirely possible (and not too hard) to make a Lean file which when opened in the VS Code Lean plugin, starts to send information via the internet and run shell commands. What it is capable of getting away with is probably largely up to the security on your computer. (In Lean 3, just write a tactic using docs3#tactic.unsafe_run_io . I assume you can still do this in Lean 4, but I don't know the secret.)

[Jason Rute]

Unlike a lot of programming languages, Lean's tactics can run when the language server is active, not just when you run the code. So it is in some ways more of a security issue than say a python program, which can't do any harm (I think) by just opening it with the python vs code plugin.

[Jason Rute]

(But on the other hand, unsafe_run_io is really useful for some projects. It lets you, for example, write tactics like lean-gptf and sagredo which interact with an external process or API.)

[Henrik Böving]

You dont need unsafe_run_io in Lean 4 that tactics can execute IO is a built in intended feature. The TacticM monad stack is on top of IO

[D. J. Bernstein]

Wojciech Nawrocki said:

Oh, hey, Joe Hendrix and I did some work on McEliece as well :) On a cursory look, djb's repo seems to be aiming at verifying the mathematics of Goppa codes and eventually McEliece. In lean-crypto, we were looking at the mostly orthogonal target of showing a concrete C implementation equivalent to a reference implementation in Lean 4.

Ultimately one wants end-to-end verification that the software is computing the specified cryptographic functions correctly on all inputs. It's clear which software matters: the machine code that the user is running. For the cryptographic functions, the optimal choice of formalization language is less obvious; we want to limit the risk of mismatches between the specification and the target of security analysis.

Whatever choice is made there, stating the end-to-end theorem requires connecting definitions of (1) instruction semantics (which maybe doesn't match real CPU behavior; see, e.g., https://lock.cmpxchg8b.com/zenbleed.html), (2) the software, and (3) the mathematical objects inside the specified cryptosystem. The proofs I posted are covering pretty much everything one needs to know about #3, but obviously they aren't saying anything about #2. Certified compilation, translation validation, etc. can connect various (#1,#2) pairs, but that still leaves a gap between #2 and #3.

In short, the software proofs and the math proofs are both needed---preferably in a single framework that can hook them together rather than leaving risks of gaps between a software-verification system and a math-verification system.

I know how to get everything done in HOL Light. I don't know how to get everything done in Lean, but I also know that I'm too new to Lean to know.

[Johan Commelin]

@D. J. Bernstein Have you also looked at Metamath Zero? The author of MM0 is @Mario Carneiro, who is an expert on both MM0 and Lean.

[D. J. Bernstein]

Johan Commelin said:

D. J. Bernstein Have you also looked at Metamath Zero? The author of MM0 is Mario Carneiro, who is an expert on both MM0 and Lean.

I looked a bit. My initial feeling, which probably says more about the documentation I found than about the actual situation, was that (1) the level of verifiability of the proofs is attractive, (2) pretty-printing modules are critical for a broad audience to tolerate reading theorem statements, and (3) the libraries are impressive in Metamath but more impressive in HOL Light, perhaps because John Harrison is very fast but perhaps because HOL Light has better tools to support efficient proof development.

[Jason Rute]

I think one needs to be careful not to mix MM0 and Metamath. If I understand correctly, MM0, while it can be used as a Metamath checker, can also be used to check other logics like HOL. I’m not entirely sure why @Johan Commelin mentioned MM0, but I think it is because of MM0’s stated goal to prove the correctness of the MM0 verifier x86 code in MM0 (using PA as the logic for verifying the verifier), but I could be mistaken.

[Jason Rute]

D. J. Bernstein said:

I know how to get everything done in HOL Light. I don't know how to get everything done in Lean, but I also know that I'm too new to Lean to know.

Would you be willing to elaborate? By “get everything done”, do you mean generate a proof that an actual working implementation of a piece of software (written in a real programming language like C++ or OCaml) is verified down to machine instructions (of the programming language? of the compiled code?) to behave as desired? I'd be surprised this is possible in any current system, including HOL-Light, but is there a way to do it in HOL-Light? (I haven't kept up to date on projects like CakeML and the such. Is there some abstract programming language in HOL Light, which can be extracted to provably correct code?)

[Jason Rute]

I guess the big problem with Lean is that while you could prove the correctness of your Lean code, and even compile it to a binary (through C++), you couldn't be sure the binary (or generated C++ code) is faithful to the mathematical Lean code for a number of reasons:

• You can't verify the wrapping IO code (I think, maybe I'm wrong).
• The Lean compiler isn't near as likely to be bug free as the Lean kernel, and certainly isn't verified to be so.
• The full Lean compilation pipeline also relies on the correctness of a C++ compiler.
• Many low level Lean data types like Nat, Array, etc are modeled with simple mathematical definitions, but replaced with native data types.
• Many low level functions are also replaced with faster C++ versions which aren't formally verified to be equivalent.

[Jason Rute]

I also don't think Lean has any form of code extraction like Coq does.

[Wenda Li]

Jason Rute said:

I'd be surprised this is possible in any current system, including HOL-Light, but is there a way to do it in HOL-Light? (I haven't kept up to date on projects like CakeML and the such. Is there some abstract programming language in HOL Light, which can be extracted to provably correct code?)

Candle is probably what you are looking for.

[D. J. Bernstein]

See CURVE25519_X25519_BYTE_SUBROUTINE_CORRECT in https://github.com/awslabs/s2n-bignum/blob/main/x86/proofs/curve25519_x25519.ml for an example of an end-to-end proof in HOL Light that some fast x86 software correctly computes a (much more simply) specified mathematical function.

[Joe Hendrix]

I agree having a framework is important. One approach I took at Galois was building equivalence checking tools for checking software matches it's specification using SAW. One tool we built in Lean was a VCG that could prove decompiled LLVM matched the semantics of x86. That tool itself is in Lean, but hasn't been formally verified itself.

[D. J. Bernstein]

Update: The HOL Light version (https://cr.yp.to/2023/lightgoppa-20230811-verify.html) is a 56997-byte gz, where the parts I'd classify as non-background are 26197 bytes. For comparison, the Lean version (https://cr.yp.to/2023/leangoppa-20230726-verify.html) is a 34067-byte gz, where non-background is 21595 bytes.

The difference between 56997 bytes and 34067 bytes is easy to explain from specific topics in basic algebra that matter for these proofs and that lightgoppa develops where leangoppa calls mathlib: e.g., deg fg = deg f + deg g for polynomials f,g in one variable over a domain. Also, in non-compressed form, lightgoppa is much more verbose than leangoppa overall, again for easy-to-explain reasons (e.g., ring_add(x_ring k) (ring_mul(x_ring k) a B) (ring_mul(x_ring k) b A) instead of a*B-b*A, and frequent this-is-an-element-of-this-ring proof steps), although this isn't a pure win for Lean (e.g., lightgoppa rarely attaches labels to hypotheses inside and outside proofs, whereas leangoppa continually does).

What' less obvious is why lightgoppa had lower elapsed time (started 31 July, so 12 days) than leangoppa (started 12 July, so 15 days), despite covering more background. Is this because I have more experience with HOL Light? Because the HOL Light proof was done second? More time was saved from HOL Light's proof automation than from Lean's proof automation? The UI was more responsive? The elapsed time doesn't reflect the actual work time?

[Mario Carneiro]

Is this because I have more experience with HOL Light? Because the HOL Light proof was done second?

These both seem very plausible answers. Second formalizations are always easier

[Mario Carneiro]

generally speaking I would put pretty big error bars on "human time spent on project" as a metric, because it is affected by things like what you were doing at the time (e.g. traveling) or your personal motivation. It is very difficult to get unbiased measurements of this, and although I don't know all the details of your month of work I would be inclined to consider this as a statistically insignificant deviation

[D. J. Bernstein]

Mario Carneiro said:

Is this because I have more experience with HOL Light? Because the HOL Light proof was done second?

These both seem very plausible answers. Second formalizations are always easier

I think all five answers (and perhaps more) are plausible, but the interesting quantitative question is how they explain the speed gap in this case, 4749 gz bytes/day for lightgoppa vs. 2271 gz bytes/day for leangoppa. If you consider the numbers I provided regarding background material then you'll see that "second formalization" has to be under half of the answer---a large part of lightgoppa is formalizing things that I hadn't formalized before, including in leangoppa!

[Mario Carneiro]

I'm absolutely sure you are more proficient in HOL light than Lean. I very much doubt you could get most of the readers of this chat to produce that HOL light code in 12 days

[Mario Carneiro]

how much HOL light code (est. lines of code) have you written prior to this project? Ditto for lean

[Mario Carneiro]

What is the compile time of the projects? Your overview page lists a time for the HOL light version (although it's not clear if this time also includes supporting material not in the project) but not the lean version

[D. J. Bernstein]

I'm new to Lean, as mentioned above. But I'm not sure how to reconcile the following hypotheses: (1) formalization in Lean is so different from formalization in HOL Light that someone with experience in HOL Light will be much slower starting out in Lean; (2) formalization in Lean is so similar to formalization in HOL Light that formalizing something in Lean will give a big speed boost to formalizing the same thing in HOL Light.

[Mario Carneiro]

Mathematically, there are a lot of similarities of course. It's the same mathematics in two languages

[Mario Carneiro]

But I would say that the formalization experience is very different, modulo the fundamental similarity of being mathematical formalizations

[D. J. Bernstein]

Are there comparative writeups somewhere?

[Mario Carneiro]

you just made one

[Mario Carneiro]

there aren't too many people with experience in both systems (I am one of them but I have not tried a comparative study, nor have I tried to do this kind of mathematics in HOL light so I'm sure there would be some more learning there)

[Mario Carneiro]

I think it is pretty good that you were able to go from ~no lean experience (I assume) to being able to formalize a complex mathematics statement with only a 2x slowdown

[D. J. Bernstein]

Mario Carneiro said:

you just made one

Well, sort of. :-) The *.ml and *.lean files don't directly say anything about formalization processes: as an extreme example, they obviously don't say anything about UI responsiveness.

[D. J. Bernstein]

(reminded of https://danluu.com/productivity-velocity/)

[Mario Carneiro]

The UI experience is pretty fundamentally different, I'm not sure numerical comparisons would even be helpful

[Mario Carneiro]

although the overall compile time number is probably useful (hence my question above)

[D. J. Bernstein]

I thought I put the compile-time numbers into both postings.

[Mario Carneiro]

https://cr.yp.to/2023/leangoppa-20230726-verify.html lacks a compile time number

[Mario Carneiro]

oh, it says "takes a few minutes"

[Mario Carneiro]

I would be interested in a more precise number to compare with the 1165 seconds number

[Mario Carneiro]

and also a clarification on whether that number includes the massive HOL startup cost

[D. J. Bernstein]

Lean is definitely much faster running through the verification: it verifies a few independent *.lean files in parallel, and doesn't run through re-verifying the standard library.

[Mario Carneiro]

do you know how to profile a HOL light project while excluding the startup cost?

[D. J. Bernstein]

1165 is for the full time ocaml ... command, as stated.

[D. J. Bernstein]

Mario Carneiro said:

do you know how to profile a HOL light project while excluding the startup cost?

Sys.time();;

[Mario Carneiro]

(I was hoping you would do it for me :smile: )

[Mario Carneiro]

actually, could you say more about your impressions re: "UI responsiveness"? My own impression is that the feedback loop in lean is worlds better than HOL light, one of the key differentiators IMO, but it's possible that you mean something more specific

[D. J. Bernstein]

80% of the theorems for this one are from the standard library (defaults plus ringtheory plus products). Probably less of the run time since the standard library puts effort into constructing proofs efficiently whereas I'm casually using model elimination at almost every step.

[Mario Carneiro]

I'm just thinking about the cost to run the code that you wrote (those 56997 bytes)

[D. J. Bernstein]

I was basically never waiting for HOL Light during proof development for this project---just a bit at the end to run through checking everything. I had much more waiting for Lean (via nvim), especially the pernicious type of waiting where there isn't an instantaneous answer and you're not sure how long you're supposed to wait.

[Mario Carneiro]

I see, so you never went backward and revised theorems?

[D. J. Bernstein]

Maybe vscode would have been better.

[Mario Carneiro]

Oh, that's an interesting point, I don't know whether there is a significant difference there as I don't use nvim

[Mario Carneiro]

Note that there are some tricks to reduce the amount of waiting, like putting #exit after the current theorem or using sorry for subproofs

[Mario Carneiro]

How long of a wait are we talking?

[Mario Carneiro]

"responsive lean" seems to be in the ballpark of 500 ms, although I know it can get much worse as you use heavier tactics

[Mario Carneiro]

This may be obvious, but lean is still under active development and people are trying to fix these kind of issues if you can isolate them and/or suggest improvements

[D. J. Bernstein]

I often ran into the default heartbeat limit. Much more often had delays of a few seconds. If I had to list the top three performance-related problems that I encountered with Lean then it'd be (1) no obvious line-by-line feedback regarding performance, (2) the search tools such as apply? apparently prioritizing some sort of completeness rather than aiming for the best quick answers, (3) any change to a proof triggering a recompilation of the proof from the top, at least with nvim. Splitting off lots of lemmas reduced the issues with #2 and #3 but of course has its own costs: some proofs are highly connected.

[D. J. Bernstein]

Mario Carneiro said:

The UI experience is pretty fundamentally different, I'm not sure numerical comparisons would even be helpful

What do you see as the big differences?

[Mario Carneiro]

Lean uses a document-style interaction mode, you can edit earlier theorems and see the effect on later ones immediately. In HOL light this means either redefining stuff and then replaying an ad hoc set of later theorems, possibly ending up in an inconsistent state, or restarting HOL light and waiting for that massive startup cost again

[Mario Carneiro]

on the flip side because HOL light is basically a REPL you get immediate feedback on the line you are currently typing

[Mario Carneiro]

(I also generally hate REPLs for the shitty text editing experience they provide by dint of being an elaborate command line interface)

[Mario Carneiro]

You can also just put your cursor anywhere and see information about proof steps, or hover and go-to-def on things, and get autocomplete. This is huge for me, and the REPL has only a poor approximation of it in that you can recall specific theorems by name

[D. J. Bernstein]

Hmmm. The HOL Light tutorial says "In fact, when I’m developing a proof in HOL I usually construct this kind of tactic script explicitly in an editor, and copy parts into the goalstack as I proceed to make sure I’m on the right track." I recently switched to the vi plugin from @Freek Wiedijk, which nicely speeds up the copy-and-paste steps.

[Mario Carneiro]

Yeah, I recall HOL4 also has some fancy things to make the copy paste part less terrible

[Mario Carneiro]

still, I think it would be a lot easier to draft such a proof if you could just see all of the intermediate steps without prompting and with live updating

[D. J. Bernstein]

Realistically, the UI ends up looking fairly similar: editor window with a proof script under development, separate window showing the goal stack (most recent assumptions at the bottom in case of overflow).

[Mario Carneiro]

that's just a technical limitation of HOL light as currently implemented, not something I consider good proof assistant design

[D. J. Bernstein]

?

[Mario Carneiro]

that was continuing my previous line

[Mario Carneiro]

That is to say, you could in principle have a more document-editor style interface even for HOL light and I think you would be able to get a faster feedback loop that way

[D. J. Bernstein]

Hmmm. My direct recent experience with the comparative UI speed seems to be the opposite of what you're saying.

[D. J. Bernstein]

To slightly oversimplify: Instantaneous feedback from HOL Light, continual random slowdowns with Lean.

[Mario Carneiro]

The other key to this being effective is that proofs have to be broken up into small self-contained units (proof steps) which are individually valid. HOL light has this (its proof mode encourages you to not write proof(... and just write top to bottom, but rather to split out each tactic into e(...) steps) but lean doesn't (you write directly into atomic theorem command blocks, and lean can only give you feedback when the whole command block is processed)

[Mario Carneiro]

In part this is a technical issue in lean, it should be able to give you feedback about the result of a tactic as soon as that tactic is complete, and it should not need to rerun tactics that have not changed since the last edit

[Mario Carneiro]

But if lean had a proof mode like HOL light's e(...) steps broken out as separate lean commands then you would certainly get back the speed benefits you are seeing in HOL Light

[Mario Carneiro]

because it's just a lot simpler to process a linear sequence of things than a complicated AST

[Mario Carneiro]

now I think I want to try to demo something like that in lean

[D. J. Bernstein]

In, e.g., goppa_closer.lean, I ended up with 20 lemmas simply trying to avoid Lean slowdowns, whereas for HOL Light I split out 4 for the same theorem.

[D. J. Bernstein]

Mario Carneiro said:

I would be interested in a more precise number to compare with the 1165 seconds number

On the same machine, 29 seconds for getting the cache, 165 seconds for building the project.

[D. J. Bernstein]

Mario Carneiro said:

Note that there are some tricks to reduce the amount of waiting, like putting #exit after the current theorem or using sorry for subproofs

For both HOL Light and Lean, I'm usually editing the last theorem in the file. (In general, I'm writing proofs bottom-up, which is always a safe way to be sure what's true, even when proof development follows other paths.) If I think a theorem really belongs somewhere else, I'll just put a move comment to handle later. For Lean, to avoid nvim crashing every few minutes, I would most often edit a theorem as a comment, and uncomment it when I wanted feedback. For HOL Light, the plugin has explicit keystrokes to request feedback.

[D. J. Bernstein]

Apparently there's progress on the nvim plugin for Lean so I might be able to skip the commenting-uncommenting part.

[D. J. Bernstein]

Meanwhile the HOL Light plugin was crashing ocaml, but that was triggered on the scale of hours and was easy to fix (fd leak). One deduces from this that I'm typically doing a goal-stack update every second or so on average.

[D. J. Bernstein]

I think this is a combination of multiple modes: often I'll type, say, 10 lines without asking for feedback; often I'll be flipping back and forth between lines while studying the list of assumptions.

[D. J. Bernstein]

Mario Carneiro said:

You can also just put your cursor anywhere and see information about proof steps, or hover and go-to-def on things, and get autocomplete. This is huge for me, and the REPL has only a poor approximation of it in that you can recall specific theorems by name

Just to advertise @Freek Wiedijk's plugin a bit more: If you put your cursor somewhere in the proof and type Ctrl-H then the separate goal-stack window shows the proof state at that point. Ctrl-P and Ctrl-N move to the previous state and the next state, while automatically moving the cursor to a logical spot.

[Julian Berman]

(The first part of that should be easily doable in nvim FWIW -- the second part we thought of I believe and want(ed) to do but I don't know if there's a more efficient way to do so in Lean than literally iterating over positions in the document and pulling the goal state, I think for something nicer there would need to be server-side support. Also in general please do feel free to file feature requests or complaints if they're nvim-specific, even though in the past year I have not gotten much time to work on things, but I very much don't mind / need some active user nagging to get to things and guilt me away from other commitments)

[Julian Berman]

To be more specific on the first bit, I'll have to try Freek's plugin, but let me know if vim.keymap.set('n', '<C-H>', require'lean.commands'.show_goal) is what you mean, or equivalently typing the command :LeanGoal (see also :LeanTermGoal)

[Julian Berman]

Which I think Gabriel added.

[D. J. Bernstein]

To mention some points where I found Lean faster than HOL Light: The Lean documentation for beginners definitely points to better discovery tools than anything I've found for HOL Light. I found autocomplete and exact? and so on helpful for learning what was available. Also, simp? serves both as a teaching tool and as a proof-speedup tool, although I'm not sure I like the way it discards the input line. @Julian Berman Thanks for fixing the ? handling, btw.

[Julian Berman]

My pleasure -- yeah feel free to complain more certainly if you notice specific things. I am myself quite bad at Lean, so I have plenty of blindspots I'm sure on what needs work -- luckily there have been others (Gabriel and Rish) who contributed and are much much much better at Lean and therefore knew what to contribute, but yeah complaints are very welcome because when I play with things I'm tinkering with simple nonsense, so it's helpful to hear when someone is doing more interesting things what needs work.

[Johan Commelin]

@D. J. Bernstein In the near future, we'll have a tactic combinator called says (I think there is a PR to mathlib underway). It will allow you to write tac1 says tac2, where tac1 can be slow, and tac2 can be fast. That way, the input line simp? will no longer need to be discarded.

An option to Lean will indicate whether says should only execute tac2 (fast mode) or whether it should execute tac1 and check that it spits out tac2 as "Try this" comment (CI mode).

[D. J. Bernstein]

Sounds perfect.

[D. J. Bernstein]

Julian Berman said:

To be more specific on the first bit, I'll have to try Freek's plugin, but let me know if vim.keymap.set('n', '<C-H>', require'lean.commands'.show_goal) is what you mean, or equivalently typing the command :LeanGoal (see also :LeanTermGoal)

Here's a small example of what the plugin looks like: https://cr.yp.to/2023/20230812/step-hol-light-example.html

[D. J. Bernstein]

For the nvim Lean plugin, the equivalent of Ctrl-H (showing the goals at the current position) is always happening as the cursor moves, and is fast enough that I'm fine with this being automatic. What's slower is editing and then waiting for Lean to recompile the proof from the top, which I gather is a general Lean limitation at the moment rather than something nvim-specific; this turns quadratic costs into cubic costs for something that I'd hope is linear cost.

[D. J. Bernstein]

I'm reminded of another Lean slowdown I encountered for some proofs: long formulas seemed to be a big speed problem. I figured that this was from Lean trying to decide what type to use for additions etc., so I inserted a bunch of type declarations, which seemed to help.

[D. J. Bernstein]

To be clear, when I say "long", I mean things like (((X:k[X])^t21*(X:k[X])*R-Q:k[X])*bar (h*q:k[X]) - ((X:k[X])^(t21)*D*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21)*(X:k[X]) * (R-bar B) * bar (h*q):k[X]):k[X]).degree, which is nowhere near the length frequently appearing in some areas of math.

[D. J. Bernstein]

(But I hear bar B is popular these days.)

[Mario Carneiro]

As far as I know there isn't anything particularly sensitive to length in the elaboration algorithm, other than basically linear costs (possibly high depending on the complexity of the typeclass problems)

[D. J. Bernstein]

Mario Carneiro said:

Lean uses a document-style interaction mode, you can edit earlier theorems and see the effect on later ones immediately. In HOL light this means either redefining stuff and then replaying an ad hoc set of later theorems, possibly ending up in an inconsistent state, or restarting HOL light and waiting for that massive startup cost again

This is something where I can quantify costs: once or twice a day I would start a separate HOL Light session to run through the whole file, and sometimes this would show that I had accidentally moved a theorem before a theorem that it depended on, so I had to move it down. But I wasn't _waiting_ for the separate HOL Light session; I was continuing to type new proofs.

Every now and then I realized that I wanted to replace an existing lemma with a generalization (this happened more often for HOL Light than for Lean since I was developing more background lemmas), and of course it's logically necessary to check all the theorems using the lemma, but this never ended up breaking anything. For Lean, any change to the hypotheses of a lemma tends to break callers using exact etc. Anyway, this wasn't a big issue overall for these proofs: the target proofs had already been written down carefully before any of the formalization, and the background was things like polynomial derivatives where everybody knows the usual proofs.

[D. J. Bernstein]

Mario Carneiro said:

(I was hoping you would do it for me :smile: )

On a 3GHz Skylake core, loading the default libraries took 97 seconds, loading further libraries took 228 seconds, and running the new proofs took 423 seconds.

[Mario Carneiro]

that doesn't seem to add up to 1165 seconds, where is the rest of the time going?

[Eric Wieser]

Mario Carneiro said:

As far as I know there isn't anything particularly sensitive to length in the elaboration algorithm, other than basically linear costs (possibly high depending on the complexity of the typeclass problems)

Does the heterogenous nature of + add to the cost here? Is lean trying to guess the final outparam from outside in after each inner expression is elaborated?

[Mario Carneiro]

binop% is supposed to fix that issue, although it's possible that there are still issues. I think this would require a contrived stress test example to determine the actual asymptotic complexity

[Scott Morrison]

Johan Commelin said:

D. J. Bernstein In the near future, we'll have a tactic combinator called says (I think there is a PR to mathlib underway). It will allow you to write tac1 says tac2, where tac1 can be slow, and tac2 can be fast. That way, the input line simp? will no longer need to be discarded.

An option to Lean will indicate whether says should only execute tac2 (fast mode) or whether it should execute tac1 and check that it spits out tac2 as "Try this" comment (CI mode).

Here "near future" is actually 2 weeks ago. :-)

[D. J. Bernstein]

https://cr.yp.to/2023/leangoppa-20230813-slower.tar.gz takes 229 seconds for lake build specifically for goppa_closer.lean (after everything else is built), where the original takes 75 seconds for that file, on a dual EPYC 7742 (128 cores, apparently using just 1 for this) running at 2.245GHz.

Compared to leangoppa-20230726, leangoppa-20230813-slower undoes various explicit :k[X] annotations and sets a much higher heartbeat limit. There are no other differences. Both builds succeed.

To be clear, this is not a contrived example: it's simply reconstructing and benchmarking one of the Lean performance problems that I encountered in formalizing the (not particularly complicated) proofs in this paper. At that point I worked around this problem rather than benchmarking it. ("I figured that this was from Lean trying to decide what type to use for additions etc., so I inserted a bunch of type declarations, which seemed to help.")

With my performance-measurement hat on, let me again emphasize the HOL Light advantage of obvious feedback on the cost of each line (specifically for model elimination, the Swiss army knife that all my have and qed lines are using). At the UI level, I'm automatically getting that feedback in a separate window (beyond the main editing window and the goal-stack window) and rapidly deal with any noticeable slowdowns (by inserting an extra have step, or adding xyzzylemma into the model elimination where I neglected to include xyzzylemma earlier). The feedback doesn't cover parsing time, but HOL Light doesn't have let's-think-hard-about-which-addition-you-really-mean built into the parser; if it did then I think I'd want that timed too. I gather that Lean has profiling tools, but nothing is on by default except for the heartbeat limit. Simply reporting the number of heartbeats used for parsing+tactics on each line should help a lot.

[Mario Carneiro]

let me again emphasize the HOL Light advantage of obvious feedback on the cost of each line

what are you referring to here?

[Mario Carneiro]

You can turn on profiling of course, if you care to see numbers; most of the time it's patently obvious what parts are slow because you have to wait for the slow parts

[Mario Carneiro]

if you put set_option profiling true lean will report on how long things take if they are above a certain threshold, which seems near to what you are describing for HOL light

[D. J. Bernstein]

Mario Carneiro said:

that doesn't seem to add up to 1165 seconds, where is the rest of the time going?

Different machine, as I said. On the EPYC, some Sys.time() outputs from a fresh run are 151.221226 505.213478 510.140727 608.500798 808.137747000000104 1170.793694 for, respectively, end of default library inclusion, end of ring-theory inclusion, end of products inclusion, start of linear-dependence proof, end of linear-dependence proof, end of all proofs.

The linear-dependence proof says (with a proof designed to be subsequently adapted into a proof of algorithm correctness) that if you're given n homogeneous linear equations in more than n variables over a domain then you can find a nonzero solution (I guess I should say "strictly more" for readers from France). This proof isn't in leangoppa since leangoppa simply puts together Lean's linearIndependent_iff_card_eq_finrank_span and finrank_le to get the field case of the same statement, and the Goppa-decoding proofs need only the field case. (_Using_ the statement was much more of a hassle, since the linear-dependence statements in Lean want finite index and coindex types while the proof in question wants degree-related polynomial exponents as index and coindex types, as we discussed in a separate thread.) What I found in the HOL Light library before writing lightgoppa was just the real case, which isn't of much use for algebraic coding theory.

[Mario Carneiro]

looks like most of the slowdown in leangoppa-slower example is caused by goppa_checking_2_lemma_hbsum6, which has its heartbeat count (as measured by count_heartbeats in) go from 1535277 (well over the default 200000) to 85821. Most of the other theorems are not in the same order of magnitude

[Mario Carneiro]

I will see if I can extract a MWE

[D. J. Bernstein]

Mario Carneiro said:

if you put set_option profiling true lean will report on how long things take if they are above a certain threshold, which seems near to what you are describing for HOL light

The level of information provided is very different. With HOL Light, what's scrolling by in the third window, by default, zero extra effort, is line-by-line model-elimination performance numbers:

  # have `ring_homomorphism(x_ring r,x_ring r) (poly_shift r (c:R))` [poly_shift_morphism]
0..0..1..solved at 4
  # qed[RING_HOMOMORPHISM_PRODUCT]
0..0..1..2..5..15..31..48..75..solved at 90

With set_option profiler true in Lean, I get various total timings for each theorem, but not line-by-line timings.

[Mario Carneiro]

here's a goppa-free MWE, still not mathlib-minimized:

import Mathlib.RingTheory.Polynomial.Basic
open Polynomial BigOperators Finset

variable {U: Type u} [DecidableEq U] {k: Type v} [Field k]
variable {α r d: U → k} {S: Finset U} {g: k[X]} {t: ℕ}

count_heartbeats in -- Used 7057 heartbeats
theorem goppa_checking_2_lemma_hbsum6_fast : True := by
  have :
    (∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ)) =
    (∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ)) := rfl
  trivial

set_option maxHeartbeats 10000000
count_heartbeats in -- Used 1606622 heartbeats
theorem goppa_checking_2_lemma_hbsum6_slow : True := by
  have :
    (∑ s in S, ∑ j in range (2*t), C ((r s / (g^2).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ)) =
    (∑ s in S, ∑ j in range (2*t), C ((r s / (g^2).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ)) := rfl
  trivial

I know that our polynomial library has some known / recurring performance issues - @Kevin Buzzard does this look familiar?

[Mario Carneiro]

@D. J. Bernstein Heavy tactics do have this kind of logging as well, and they will show up in the profiler. It's just that we have fewer of them; the lack of a METIS_TAC/ qed equivalent is a long standing open problem for mathlib

[Mario Carneiro]

minimized some more:

import Mathlib.RingTheory.Polynomial.Basic
open Polynomial BigOperators Finset

variable {k: Type v} [Field k] {α: k} {S: Finset ℕ} {g: k[X]}

count_heartbeats in -- Used 6637 heartbeats
theorem goppa_checking_2_lemma_hbsum6_fast : True := by
  have :
    (∑ _s in S, ∑ _s in S, C (1 * (g^2:k[X]).eval α * 1)) =
    (∑ _s in S, ∑ _s in S, C (1 * (g^2:k[X]).eval α * 1)) := rfl
  trivial

set_option maxHeartbeats 2000000
count_heartbeats in -- Used 1076105 heartbeats
theorem goppa_checking_2_lemma_hbsum6_slow : True := by
  have :
    (∑ _s in S, ∑ _s in S, C (1 * (g^2).eval α * 1)) =
    (∑ _s in S, ∑ _s in S, C (1 * (g^2).eval α * 1)) := rfl
  trivial

[Mario Carneiro]

Hm, using g*2 instead of g^2 is fast, as is HPow.hPow g 2 instead of g^2. So I think this is pointing a finger at the erroneous usage of binop% for the power function, cc: @Kyle Miller

[D. J. Bernstein]

Mario Carneiro said:

D. J. Bernstein Heavy tactics do have this kind of logging as well, and they will show up in the profiler. It's just that we have fewer of them; the lack of a METIS_TAC/ qed equivalent is a long standing open problem for mathlib

I'm actually using MESON rather than METIS. Either way, from a user perspective it's super-convenient to be able to just list all the relevant lemmas and have the computer figure out the logic of putting them together. The computation is very fast in most of the cases where simpler tactics would work. Of course there are also situations better handled by rw or simp or Lean's aesop, but most of the lightgoppa proof steps are model elimination.

[Mario Carneiro]

The WIP tactic for this in lean is duper, but in a recent discussion with @Jeremy Avigad it came up that we don't have too many example uses and the authors are having difficulty determining what sort of things need to be supported, so if you could give some examples that would be very helpful.

[D. J. Bernstein]

Again, every have step in the lightgoppa proofs is model elimination!

[Mario Carneiro]

yes, but HOL light uses a different proof style which is more statement-centric. Maybe you could mock up what you would want to write in the lean proof such that model elimination plays a bigger role?

[Mario Carneiro]

Actually, I'm not sure I know what you mean by "model elimination". This is an SMT solver, is it not?

[D. J. Bernstein]

https://www.cl.cam.ac.uk/~jrh13/atp/OCaml/meson.ml is a MESON introduction.

[D. J. Bernstein]

I'm not sure what you mean by "statement-centric". Pretty much every exact and apply step in leangoppa is something that I would rather have expressed with model elimination.

[Mario Carneiro]

I see very few exact and apply in e.g. goppa_closer, you seem to like calc proofs a lot

[D. J. Bernstein]

Obviously by exact is eliminated so you need to do more than grep to see what's going on. Beyond the exact and apply steps, many of the sequences of rewriting tactics would have been handled just as easily by model elimination. Yes, I tend to use declarative proofs, and calc is a win for that.

[D. J. Bernstein]

On second thought, grep used as follows gives some idea of what's going on, namely 361 lines of output: grep ':= .' Goppadecoding/*.lean | grep -v ':= by'

The fact that exact? can find these is also what makes model elimination work instantly for them. The big advantage of model elimination is that it can handle multiple steps at once. The model-elimination user supplies the list of lemmas but doesn't have to bother spelling out the connecting logic or which hypotheses to plug in.

[Scott Morrison]

Mathlib's closest approximation to this is solve_by_elim. exact? is just trying out every relevant library lemma, and then calling solve_by_elim to discharge the subgoals. You can call solve_by_elim [X, Y, Z] manually to give it extra lemmas, or have := X ahead of an an exact? to allow the library search step to use X in tackling subgoals.

[D. J. Bernstein]

I'll give that a try, thanks.

[D. J. Bernstein]

Passing along some comments from John Harrison on MESON:

I originally implemented it precisely to act in the way you are
using it, plugging together other theorems in straightforward
but mildly fiddly ways in support of a more declarative style of
proof. See the little paragraph "a model elimination prover" on
p13 here:

https://www.cl.cam.ac.uk/~jrh13/papers/mizar_times.pdf

The underlying model elimination idea was invented by Loveland in
the context of linear resolution, and recast by Stickel, Plaisted
and others into a form that is a fairly small tweak to Prolog-type
backchaining while still being complete for first-order logic
(which Prolog is not, even if you do complete search instead of
depth-first). Of course, my associated book "Handbook of Practical
Logic and Automated Reasoning" explains the code you pointed to in
more detail, while this is the sub-reference [18] from that paragraph
above talks about the implementation details:

https://www.cl.cam.ac.uk/~jrh13/papers/me.pdf

It doesn't discuss proof generation in HOL Light, but as usual
with these search-dominated procedures that's fairly trivial/obvious.
I'm sure Mario could produce a Lean version in a long weekend ;-)

[Mario Carneiro]

I'm sure Mario could produce a Lean version in a long weekend ;-)

heh, I've already started

[D. J. Bernstein]

https://cr.yp.to/papers.html#goppadecoding now compares its informal theorem statements to formalizations in Lean (and in HOL Light), and includes a partial review of the underlying definitions. This isn't about the formalization process beyond the outputs; I'm planning a separate writeup of observations regarding the process.

[Oisin McGuinness]

D. J. Bernstein said:

now compares its informal theorem statements to formalizations in Lean (and in HOL Light)

The format for this is really excellent, left and right columns with corresponding code and math! Very helpful!

[Patrick Massot]

I had a quick look at the paper and I have one important remark: it seems you systematically use the word Lean when you want to write Mathlib. A typical sentence doing that is "Lean defines an equivalent function under the name monomial". In fact it seems the word Mathlib does not appear in the paper. I only read very superficially so I cannot say whether this is crucial anywhere. But it could be, especially since you write for computer scientists that could be interested in constructive math or computability (which are almost totally ignored by Mathlib but fully supported by the Lean kernel).

[Patrick Massot]

You also have strange sentences about what polynomials are in mathematics such as "Mathematically, multivariate polynomials over a ring r are functions from exponent vectors to r satisfying certain finiteness conditions." and "Presumably what will be best in the long run is a formalized version of what appears in the mathematical literature: a simple definition of univariate polynomial rings, a more complicated definition of multivariate polynomial rings, and theorems regarding the relationship between the definitions.". This may match the way you were taught polynomials, but this is far from being universal. You would have a hard time matching these sentences to how Bourbaki defines polynomials for instance.

[Patrick Massot]

Note these are comments and improvement suggestions that may sound like criticisms but this isn't my goal. And overall this paper looks very interesting to me (although I don't see why you would care about this information).

[Eric Wieser]

From page 47:

Lean also provides natDegree producing results in N, in particular mapping
0 to 0.

I assume this should read "$-\infty$ to 0"

[Mario Carneiro]

no, I think it means mapping the zero polynomial to natDegree 0

[D. J. Bernstein]

Patrick Massot said:

I had a quick look at the paper and I have one important remark: it seems you systematically use the word Lean when you want to write Mathlib. A typical sentence doing that is "Lean defines an equivalent function under the name monomial". In fact it seems the word Mathlib does not appear in the paper. I only read very superficially so I cannot say whether this is crucial anywhere. But it could be, especially since you write for computer scientists that could be interested in constructive math or computability (which are almost totally ignored by Mathlib but fully supported by the Lean kernel).

Thanks for the comment. Given that https://leanprover-community.github.io/ describes mathlib as "the Lean mathematical library", I think it's appropriate to attribute mathlib's definitions to Lean. There are a few cases where the internal structure of proof assistants is relevant to the text, and for those cases I'm using assistant-independent terminology such as "kernel"; I'm trying to avoid flooding the reader with assistant-specific terminology.

[Scott Morrison]

I agree with Patrick that this is wrong. Lean is a programming language that happens to be excellent for doing formalised mathematics. Mathlib is by a large margin the largest mathematical library written in Lean, and hence may be called "the Lean mathematical library". Moreover Lean the language is both informed by the needs of Mathlib, and wants to support it.

But Mathlib is not Lean, nor a part of Lean, and I think just basic academic standards of attribution argue against "it is appropriate to attribute mathlib's definitions to Lean".

[Henrik Böving]

Note that the group of people that develop Lean 4 and the group of people that develop Mathlib 4 does only have a very small intersection so most things that are done in Mathlib 4 happen without influence by the Lean 4 developers.

[Kevin Buzzard]

@D. J. Bernstein the reason that it was feasible to do your project in lean is because of mathlib. Note that the lean 4 repo is owned by GitHub user leanproverwhich is AFAIK Leo or Microsoft or whatever, but the mathlib is owned by leanprover-community, which is a community-led project consisting of the people you see here who answer your questions for free and are building an amazing product.

[D. J. Bernstein]

Patrick Massot said:

You also have strange sentences about what polynomials are in mathematics such as "Mathematically, multivariate polynomials over a ring r are functions from exponent vectors to r satisfying certain finiteness conditions." and "Presumably what will be best in the long run is a formalized version of what appears in the mathematical literature: a simple definition of univariate polynomial rings, a more complicated definition of multivariate polynomial rings, and theorems regarding the relationship between the definitions.". This may match the way you were taught polynomials, but this is far from being universal. You would have a hard time matching these sentences to how Bourbaki defines polynomials for instance.

Um, have you actually read Bourbaki's definition?

The polynomial A-algebra on I is defined at the beginning of Algebra 4 as the free commutative A-algebra on I. That's defined on page 448 of (the English translation of) Algebra 1-3 as the A-algebra of the free commutative monoid on I. The free commutative monoid on I is defined on page 92 as finitely supported vectors indexed by I with entries in \N. The A-algebra of S is defined on page 446 as the finitely supported vectors indexed by S with entries in A.

So, with the terminology unfolded, that's the finitely supported A-vectors indexed by finitely supported vectors indexed by I with entries in \N. How exactly do you believe this isn't consistent with "multivariate polynomials over a ring r are functions from exponent vectors to r satisfying certain finiteness conditions"?

[D. J. Bernstein]

Patrick Massot said:

Note these are comments and improvement suggestions that may sound like criticisms but this isn't my goal. And overall this paper looks very interesting to me (although I don't see why you would care about this information).

Sorry, can you clarify which information you're referring to?

[D. J. Bernstein]

Scott Morrison said:

But Mathlib is not Lean, nor a part of Lean

Please clarify. It's okay to talk about mathlib as Lean's mathematics library and to talk about "Lean's mathlib", but the possession concept here isn't transitive---mathlib is Lean's mathlib, and mathlib's X is Lean's mathlib's X, but isn't Lean's X?

[D. J. Bernstein]

Kevin Buzzard said:

D. J. Bernstein the reason that it was feasible to do your project in lean is because of mathlib. Note that the lean 4 repo is owned by GitHub user leanproverwhich is AFAIK Leo or Microsoft or whatever, but the mathlib is owned by leanprover-community, which is a community-led project consisting of the people you see here who answer your questions for free and are building an amazing product.

Poking around, I find DBLP:conf/cpp/X20, which of course I'm happy to cite.

[D. J. Bernstein]

Current draft: See \cite{1996/harrison} for an introduction to HOL Light, \cite{2021/moura} for an introduction to Lean 4, and \cite{2020/mathlib} for an introduction to the Lean math library. This appendix says ``HOL Light'' and ``Lean'' to refer to the full proof assistants available when these formalizations began, including the math libraries.

When I'm pointing out that, e.g., Lean automatically understands (0:K)^{-1} = 0 to have the second 0 meaning 0:K, I think it's an active disservice to the reader to try to explain my current understanding of how this feature is decomposed between language structures and library structures. If saying "Lean" here triggers offense because of some sort of credit battle between the language and the library, then I would suggest adding documentation on the preferred terminology for referring to the full package.

[Mario Carneiro]

D. J. Bernstein said:

Scott Morrison said:

But Mathlib is not Lean, nor a part of Lean

Please clarify. It's okay to talk about mathlib as Lean's mathematics library and to talk about "Lean's mathlib", but the possession concept here isn't transitive---mathlib is Lean's mathlib, and mathlib's X is Lean's mathlib's X, but isn't Lean's X?

Just use "Mathlib" where you have used "Lean". Mathlib can be (and should be) used as a proper noun to describe "Lean's mathematical library" (where "mathematical library" is not a proper noun); "Lean's mathlib" sounds a bit odd. Elsewhere, when describing properties of the library, attribute them to "mathlib", not "lean".

[Mario Carneiro]

D. J. Bernstein said:

When I'm pointing out that, e.g., Lean automatically understands (0:K)^{-1} = 0 to have the second 0 meaning 0:K, I think it's an active disservice to the reader to try to explain my current understanding of how this feature is decomposed between language structures and library structures. If saying "Lean" here triggers offense because of some sort of credit battle between the language and the library, then I would suggest adding documentation on the preferred terminology for referring to the full package.

The preferred terminology is "mathlib". A natural way to rephrase your sentence is: "Mathlib automatically understands (0:K)^{-1} = 0 to have the second 0 meaning 0:K". Lean has very little to do with almost anything in this sentence, that's entirely library choices you are talking about.

[Mario Carneiro]

Although, you could also try personifying these systems less so that you don't need to use active voice and cause this issue

[Mario Carneiro]

"In lean, the second 0 of (0:K)^{-1} = 0 is interpreted as meaning 0:K" seems fine to me, but not "Lean defines multivariate polynomials as ...." because mathlib is the one doing the defining, not lean

[D. J. Bernstein]

Mario Carneiro said:

D. J. Bernstein said:

Scott Morrison said:

But Mathlib is not Lean, nor a part of Lean

Please clarify. It's okay to talk about mathlib as Lean's mathematics library and to talk about "Lean's mathlib", but the possession concept here isn't transitive---mathlib is Lean's mathlib, and mathlib's X is Lean's mathlib's X, but isn't Lean's X?

Just use "Mathlib" where you have used "Lean". Mathlib can be (and should be) used as a proper noun to describe "Lean's mathematical library" (where "mathematical library" is not a proper noun); "Lean's mathlib" sounds a bit odd. Elsewhere, when describing properties of the library, attribute them to "mathlib", not "lean".

I appreciate the suggestions, but I'm also really confused at this point, given, e.g., that https://arxiv.org/abs/2108.10700 says "Lean's mathlib" in its title, and that https://xenaproject.wordpress.com is continually saying things like "Lean for the curious mathematician" with no evident backlash.

If it's wrong for me to attribute definitions of (say) polynomials to Lean, then why is it okay for https://xenaproject.wordpress.com/what-maths-is-in-lean/ to list polynomials as an answer to the question "What maths is in Lean?"? Sure, that was in 2019, but "What maths is in Lean?" is listed as one of the featured tabs on top of the page, and there doesn't seem to be an erratum anywhere saying that the terminology was wrong.

Regarding the idea of just saying "mathlib" everywhere, I'm more than a bit skeptical that this is accurate in, e.g., Here is how to run {\tt leangoppa} in Lean.; In both HOL Light and Lean, the universe is partitioned into disjoint ``types''.; the Lean syntax often allows the map from $\N$ to $\Z$ to be left implicit; Lean automatically using the desired function; etc.

More generally, the text is describing user-visible features of the language-plus-library bundle that I was using. I'm going to use one name for that bundle, and I'm not going to allow the text to be sidetracked into irrelevant internal details (even on the occasions where I'm pretty sure I know those details). If "Lean" causes confusion as a name for the bundle then it's hard to imagine that the opposite extreme of "mathlib" fixes the problem. How about "LUM", for "Lean union mathlib"?

[D. J. Bernstein]

Scott Morrison said:

I think just basic academic standards of attribution argue against "it is appropriate to attribute mathlib's definitions to Lean".

To make sure I understand, you're saying the title "What maths is in Lean?" of https://xenaproject.wordpress.com/what-maths-is-in-lean/ is violating "basic academic standards of attribution" by saying that algebra etc. are "in Lean"?

[Eric Wieser]

I think that title should be read as "what maths has been written in Lean", not "what maths does Lean provide"

[Mario Carneiro]

"Lean for the curious mathematician" is also a "brand name" of a sort, it is the title of a conference that has been held for several years.

[Mario Carneiro]

Regarding the idea of just saying "mathlib" everywhere, I'm more than a bit skeptical that this is accurate in, e.g.,
* Here is how to run {\tt leangoppa} in Lean

This is just a weird sentence to say, you can't run it in anything else, can you? You aren't running it "in mathlib" in any case.

• In both HOL Light and Lean, the universe is partitioned into disjoint "types"

Agreed, this is a property of Lean, not mathlib.

• the Lean syntax often allows the map from $\N$ to $\Z$ to be left implicit

This is also a property of lean. Certainly "Lean syntax" is more correct than "mathlib syntax" as mathlib doesn't define syntax (well it kind of does, but I would generally describe that as "notation" rather than "syntax")

• Lean automatically using the desired function

This one is borderline, but I would probably prefer to use "lean" here.

The fact is that there are things that lean does and things that mathlib does, and you should try to attribute things correctly because they are different entities. I realize this might be challenging, but similar situations do exist in most other theorem provers as well. HOL light bundles its library with the language, but if for example you were writing about a project that depends on the Flyspeck formalization, you should differentiate between definitions that came from the Flyspeck part and things that came from the base library. Same thing with AFP vs Isabelle/HOL vs Isabelle/Pure, or metamath vs set.mm, or Mizar vs MML, or the Coq standard library vs mathcomp.

[Mario Carneiro]

It's true that you shouldn't attribute everything to mathlib, nor everything to lean. If you can't be bothered to differentiate you could use Lean/mathlib, but generally that seems like lazy writing and in each individual instance you should use the right one. It's mostly not too hard since when talking about language behaviors it's lean and when talking about definitions and library objects (especially when commenting on the form of definitions and how easy/difficult they are to work with) it's mathlib you are talking about.

[D. J. Bernstein]

Mario Carneiro said:

The fact is that there are things that lean does and things that mathlib does, and you should try to attribute things correctly because they are different entities.

There are also things that various compiler layers do, things that the OS does, things that the CPU does, things that the RAM does, etc. Those are different entities. Ergo, anyone writing about Lean should separately attribute those things? Does one mention of AMD and zero mentions of the RAM manufacturer really do justice to their critical contributions here?

I also don't understand why you think it's incorrect to attribute behavior to the unified system, when the observed and easily reproducible and relevant facts are that the unified system is behaving as described. Referring to verifiability as laziness doesn't help your case.

Regarding terminology for the unified system, I've now reviewed enough material to be sure that I made the correct choice for this paper. If I see consistent, stable, documented renaming of "Lean for the curious mathematician", "What maths is in Lean", "Learning Lean", etc., I'll be happy to adjust my future use of terminology to match. To answer your question, I've run leangoppa in some ad-hoc tools that I wrote that of course test vastly less than Lean does, whereas obviously what matters at this point in the paper is the level of assurance obtained by running it in Lean.

[Patrick Massot]

D. J. Bernstein said:

Um, have you actually read Bourbaki's definition?

The polynomial A-algebra on I is defined at the beginning of Algebra 4 as the free commutative A-algebra on I. That's defined on page 448 of (the English translation of) Algebra 1-3 as the A-algebra of the free commutative monoid on I. The free commutative monoid on I is defined on page 92 as finitely supported vectors indexed by I with entries in \N. The A-algebra of S is defined on page 446 as the finitely supported vectors indexed by S with entries in A.

So, with the terminology unfolded, that's the finitely supported A-vectors indexed by finitely supported vectors indexed by I with entries in \N. How exactly do you believe this isn't consistent with "multivariate polynomials over a ring r are functions from exponent vectors to r satisfying certain finiteness conditions"?

Yes, I am very familiar with Bourbaki's definition. And if you unfold all constructions then you indeed get there. This is exactly why I always teach this as an example of how meaning is lost if you unfold too many definitions in math. Note I wrote that writing "polynomials are ..." is strange (rather than wrong). You are really insisting on implementation details here. And even unfolding definitions, I don't see "a simple definition of univariate polynomial rings, a more complicated definition of multivariate polynomial rings, and theorems regarding the relationship between the definitions" in there.

But I don't think there is much point in continuing this specific discussion. I clearly failed to convey the tone I intended for this remark (despite my attempt in the following message). I don't want you to feel attacked, especially since this is a really very minor point. I probably shouldn't have raised it.

[Patrick Massot]

D. J. Bernstein said:

Patrick Massot said:

Note these are comments and improvement suggestions that may sound like criticisms but this isn't my goal. And overall this paper looks very interesting to me (although I don't see why you would care about this information).

Sorry, can you clarify which information you're referring to?

The information that I think your paper looks very interesting. Probably I shouldn't have tried to write all this in English while being so tired.

[Scott Morrison]

D. J. Bernstein said:

Scott Morrison said:

I think just basic academic standards of attribution argue against "it is appropriate to attribute mathlib's definitions to Lean".

To make sure I understand, you're saying the title "What maths is in Lean?" of https://xenaproject.wordpress.com/what-maths-is-in-lean/ is violating "basic academic standards of attribution" by saying that algebra etc. are "in Lean"?

A post from 2019, whose first line is "NB: A more up to date list of what is in mathlib is here on the leanprover-community website." seems pretty funny as evidence that everyone conflates Lean and Mathlib, and that it is a good thing to continue doing so, in my mind. :woman_shrugging:

[D. J. Bernstein]

Patrick Massot said:

And even unfolding definitions, I don't see "a simple definition of univariate polynomial rings, a more complicated definition of multivariate polynomial rings, and theorems regarding the relationship between the definitions" in there.

The text at hand correctly states that this is "what appears in the mathematical literature". It doesn't make absurd claims about arbitrary nonempty subsets of the literature.

As for the multivariate definition, I've provided pinpoint citations trivially matching up Bourbaki's definition to the description I gave, so please withdraw the claim that "You would have a hard time matching these sentences to how Bourbaki defines polynomials".

Given your background and your comment about "implementation details", I presume that what you were actually thinking of from the beginning was initial pointed rings---which, sure, _can_ be converted from a predicate into a construction via the generic universal-algebra construction of free objects, but that's _not_ how polynomial rings are defined in Bourbaki or in mainstream commutative algebra.

I remember having fun teaching a commutative-algebra course 25 years ago. I started by proving that the usual finite axiomatization of a (commutative) ring implies that rings satisfy all (0,1,-,+,*) identities satisfied by \Z, the latter statement being defined via the usual concrete definition of multivariate polynomials and proven via freeness (along with some facts about \Z). This also shows en passant that the concrete objects are isomorphic _as pointed rings_ to the generic universal-algebra free objects. But this doesn't mean these are defining the same objects!

The big advantage of the concrete definition, beyond its accessibility, is that it's directly equipped with helpful structure beyond the ring structure. Proofs in the literature are continually taking advantage of this structure, even when the objective is purely to prove a general ring statement that makes no reference to this structure. Every proof mentioning a power-series coefficient, or in particular a polynomial coefficient, is directly referring to this structure. So I would question the competence of anyone objecting to the concrete definition.

[D. J. Bernstein]

Scott Morrison said:

D. J. Bernstein said:

Scott Morrison said:

I think just basic academic standards of attribution argue against "it is appropriate to attribute mathlib's definitions to Lean".

To make sure I understand, you're saying the title "What maths is in Lean?" of https://xenaproject.wordpress.com/what-maths-is-in-lean/ is violating "basic academic standards of attribution" by saying that algebra etc. are "in Lean"?

A post from 2019, whose first line is "NB: A more up to date list of what is in mathlib is here on the leanprover-community website." seems pretty funny as evidence that everyone conflates Lean and Mathlib, and that it is a good thing to continue doing so, in my mind. :woman_shrugging:

Please clarify. If attributing mathlib's definitions to Lean violates "basic academic standards of attribution", should I conclude that the "What maths is in Lean?" title of this 2019 posting was violating "basic academic standards of attribution"? If not, why not? How about the continued highlighting of that title as a tab on the same site, as mentioned above? Needless to say, proper attribution is an ethics requirement, and claims of improper attribution should be resolved.

[Mario Carneiro]

It is indeed imprecise wording at best, and would definitely be more accurately written as "What maths is in mathlib?". Whether this rises to the level of misconduct is questionable, but it is not an academic paper and it is also only a title, targeted at people who may not yet know the difference. There is still plenty of space to be more precise in the body text, and indeed the very first line when I click through says "what is in mathlib".

[Mario Carneiro]

D. J. Bernstein said:

Mario Carneiro said:

The fact is that there are things that lean does and things that mathlib does, and you should try to attribute things correctly because they are different entities.

There are also things that various compiler layers do, things that the OS does, things that the CPU does, things that the RAM does, etc. Those are different entities. Ergo, anyone writing about Lean should separately attribute those things? Does one mention of AMD and zero mentions of the RAM manufacturer really do justice to their critical contributions here?

Yes of course they should be attributed if their behavior is relevant. If a proof verifies on AMD and not on Intel then of course you should say these things. If the CPU is not relevant or you are not talking about it, then you should not.

Same thing applies here. If you are talking about lean, you should use "lean" as the subject of the sentence, and if you are talking about mathlib then you should use "mathlib" as the subject of the sentence. If you are talking about the CPU then say that. This is not about acknowledging their "critical contributions", that's what citations are for and you've done that well enough already. This is just about using the correct subjects for sentences to identify distinct entities correctly.

I also don't understand why you think it's incorrect to attribute behavior to the unified system, when the observed and easily reproducible and relevant facts are that the unified system is behaving as described. Referring to verifiability as laziness doesn't help your case.

It would be incorrect to attribute the definition of multivariate polynomials to Intel too. They had no hand in the matter. Saying "the computer" or "Intel/AMD/Lean/Mathlib" doesn't help anything, there is exactly one party involved in the definition of multivariate polynomials relevant to the discussion and not looking up which one it is and saying all of them is lazy writing. And saying "Lean" is misattribution, as you have omitted the relevant party. In some places and times you might be able to get away with such misattribution, but an academic paper is not one of them and if I was a reviewer of your paper this would be a blocking concern.

[Kevin Buzzard]

I don't think that some random blog post I wrote years ago when I was just finding my feet should be used as evidence for anything

[Mario Carneiro]

I suspected you would say that, but didn't want to put words in your mouth :smile:

[Kevin Buzzard]

Sorry, I've only had very limited internet access for the last week

[Mario Carneiro]

FWIW @D. J. Bernstein your post has triggered a bit of an audit of our teaching materials to make sure we haven't made this slip-up elsewhere. You might be able to dig up some examples but that doesn't mean they are recommended practice. (The other examples you gave, LFTCM and "learning lean", seem to be using the word "lean" correctly, even if lean isn't the only thing on the agenda.)

[Eric Wieser]

D. J. Bernstein said:

but I'm also really confused at this point, given, e.g., that https://arxiv.org/abs/2108.10700 says "Lean's mathlib" in its title

My intention in this phrasing was to convey "Mathlib, the library for lean", in the same way as I might say "Python's numpy" or "C++'s Eigen"; the phrasing is certainly ambiguous, but a fully unambiguous title would have been too long for my taste. The main text clarifies the relationship in the first sentence, just as Kevin's blog post does.

[Mario Carneiro]

it is a bit of an unfortunate truth that "mathlib" without additional context is somewhat unclear to the uninitiated - it looks like an abbreviation of "math library" (and it is), but a math library for what? In practice, it is used more as a proper noun, and it isn't really correct to unpack it as "math library" any more than one would unpack "microsoft" as "microcomputer software"

[Mario Carneiro]

hence one will generally have to specify with qualifiers like "lean's mathlib" or "the lean mathematical library" when giving titles and other zero-context introductions

[D. J. Bernstein]

Mario Carneiro said:

The other examples you gave, LFTCM and "learning lean", seem to be using the word "lean" correctly, even if lean isn't the only thing on the agenda.

I find it crystal clear that these sources are using "Lean" to refer to the core-language-plus-library bundle. If a reader is, despite the available documentation, somehow coming to a "Lean" course with the idea that "Lean" refers only to the Lean core language and not also to Lean's math library, and is then told a little bit about the core language and much more about the library, then the reader is forced to conclude that either (1) the idea was wrong or (2) the course was mislabeled.

Saying something like "No, look, you also learned something about the core language" is like claiming that an "Introduction to Python" book actually means "Python" as just the core language and not also the libraries, despite most of the book being about library features.

[Mario Carneiro]

Okay, but again this is just branding. It does not justify incorrect usage of terms in an academic paper

[Mario Carneiro]

Sure, the course is mislabeled. Does this help clarify the situation?

[Eric Wieser]

FWIW, the first "intro to python book" I found a contents page for is genuinely only about the core language and standard library. I think it's important to note that mathlib is not the standard library in the same sense as subprocess or json are in python.

[D. J. Bernstein]

"This is a online interactive tutorial to Lean focused on proving properties of the elementary operations on natural numbers"

[D. J. Bernstein]

"the standard mathematics oriented reference is Mathematics in Lean"

[D. J. Bernstein]

"This repository is an introduction to theorem proving in Lean for the impatient"

[Eric Wieser]

D. J. Bernstein said:

"This is a online interactive tutorial to Lean focused on proving properties of the elementary operations on natural numbers"

I think this is mostly correct, the natural number game uses approximately no mathlib

[D. J. Bernstein]

"Approximately no" sounds like nonzero to me.

[Eric Wieser]

D. J. Bernstein said:

"the standard mathematics oriented reference is Mathematics in Lean"

This is accurate; the second paragraph of the intro says "This tutorial is based on Lean’s large and ever-growing library, Mathlib.". This is akin to titling a book "data science in python", and then proceeding to use numpy througout even though you didn't feature it in the title.

[Kevin Buzzard]

@D. J. Bernstein I've been in a field for the best part of a week and I'm now just catching up and am very surprised to see this conversation still continuing. A bunch of people have told you that you're not citing mathlib correctly and my impression is that all you're doing is spending days and days clutching at straws and attempting to find examples which do things like you (often written by me in 2018 when the lean community was a completely different place) without ever mentioning the far larger body of literature which is citing mathlib correctly. If you really don't want to give credit to the library you used despite having this spelt out to you then I guess that's fine, although it is also a bit unprofessional. If you want to continually search the internet for evidence that your view is correct despite the community continually explaining to you that it is not then I'm not sure you're going to get anywhere.

[D. J. Bernstein]

Um, there hasn't been any evident change since 2018. There's pervasive, continuing use of "Lean" to refer to the whole bundle. Finding a massive pile of examples takes no effort.

[D. J. Bernstein]

"Induction in Lean isn’t just something which you do on natural numbers"

[Eric Wieser]

That one is genuinely about Lean, induction is a builtin tactic, as are the natural numbers

[D. J. Bernstein]

"A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant"---gee, why not "using mathlib"?

[D. J. Bernstein]

"The corresponding statement in Lean is the following"---why no credit here to mathlib?

[D. J. Bernstein]

"The success of the project is the result of the hard work of many people in the Lean community"---why not also "the mathlib community"?

[Kyle Miller]

I'd say the mathlib community is a subset of the Lean community.

[Kyle Miller]

D. J. Bernstein said:

"A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant"---gee, why not "using mathlib"?

This is like saying "we wrote a program in Javascript" even though you're surely pulling in any number of libraries.

[D. J. Bernstein]

"the status of algebraic geometry in Lean"---why not "in mathlib"?

[D. J. Bernstein]

"They also created evidence for Lean’s Ext groups, profinite spaces, condensed abelian groups and so on"---why not mathlib's Ext groups?

[Kyle Miller]

D. J. Bernstein said:

"the status of algebraic geometry in Lean"---why not "in mathlib"?

The mathlib project is part of the greater Lean project in terms of the community's attention. If mathlib has something formalized, then "Lean" in a very informal sense has it formalized. It would be more accurate to say that mathlib has algebraic geometry certainly.

[D. J. Bernstein]

A paper saying "Lean defines ..." is being accused of inaccuracy and academic misconduct, but meanwhile it's okay to say "Lean's Ext groups"? Seriously?

[Eric Wieser]

The Ext group in question here resides in LTE itself (which the blog post is about), not in mathlib

[Kyle Miller]

Sorry, at what point was there an accusation of misconduct?

[D. J. Bernstein]

Eric Wieser said:

The Ext group in question here resided in LTE itself (which the blog post is about), not in mathlib

So attributing LTE's definitions to Lean is okay, while attributing mathlib's definitions to Lean isn't?

[Kyle Miller]

I don't think "Lean's Ext groups" is a good description. Note that this is again Kevin's blog, where he has an explicit disclaimer: "I am not speaking for all the authors or the Lean community or the mathlib community or any other organization"

[D. J. Bernstein]

Kyle Miller said:

Sorry, at what point was there an accusation of misconduct?

"I think just basic academic standards of attribution argue against "it is appropriate to attribute mathlib's definitions to Lean"."; "you should try to attribute things correctly"; "If you really don't want to give credit to the library you used ... a bit unprofessional"

[Kyle Miller]

Oh, sure. I see people have also given you examples in other languages and systems.

I wouldn't bat an eye at a course called "Numerical linear algebra in Python" and then it being all about how to use numpy. I would be surprised if someone used numpy in a paper and insisted on saying things like "Python defines numpy.array." That seems like it would be confusing, and I'd imagine it might rub the numpy developers the wrong way.

Just in case you're not aware, the people objecting to attributing mathlib definitions to Lean itself are all mathlib contributors. We might not be consistent with it, but despite all the mistakes you've found that are out there, I think we all generally want to distinguish Lean and mathlib.

[Kyle Miller]

At least this mathlib contributor would be happy with "Lean defines an equivalent function under the name monomial" -> "The Lean mathematical library mathlib defines an equivalent function under the name monomial".

[Eric Wieser]

I'd imagine it might rub the numpy developers the wrong way.

With my numpy maintainer hat on, I agree

[Arthur Paulino]

Let me also risk saying this: my impression is that the distinction between Lean and Mathlib became clearer with time, especially with the advance of Lean 4. Back in the days, leanprover-community had to maintain its own fork of Lean 3 in order to keep Mathlib evolving. Not that it causes confusion, but it can contribute to historical blurriness since the ones developing Lean 3 in practice were, for a while, Mathlib maintainers. The scenario is very different now with Lean 4, which is pretty new to the community. And your publication can be a force that pushes future writers towards more precise writing.

And I also want to say this: I don't think you're indulging in any form of misconduct. To me, it's just that the community is adapting/evolving, very much like Lean and Mathlib themselves.

[Mauricio Collares]

Two cents from an outsider: I do understand that people want proper attribution and that's great, but the GItHub organization is called leanprover-community, the community Zulip is called leanprover.zulipchat.com, and the project is called "Lean mathematical library". I honestly thought it was a deliberate attempt at creating a unified identity, even after following the project for a couple of years and knowing that the two parts are developed by an almost disjoint set of people.

[Bulhwi Cha]

Kyle Miller said:

I'd say the mathlib community is a subset of the Lean community.

We might have Lean libraries for subjects other than mathematics in the future. At least, I hope so.

[D. J. Bernstein]

Kyle Miller said:

I don't think "Lean's Ext groups" is a good description. Note that this is again Kevin's blog, where he has an explicit disclaimer: "I am not speaking for all the authors or the Lean community or the mathlib community or any other organization"

I'm not sure why this disclaimer is relevant here. Is there a URL somewhere where I can see some of those other people stating that "Lean's Ext groups" was inappropriate attribution and incorrect attribution and unprofessional?

There's this mountain of examples of the word "Lean" obviously being used to include not just the core language but also the math library. This provides a perfectly straightforward explanation for mathlib-oriented courses and workshops being labeled as "Lean" courses and workshops, for wording such as "Lean's Ext groups" (the distinction between mathlib and prototypes isn't relevant here), for wording going out of its way to refer specifically to the core language when that's relevant (such as "If you are interested in Lean as a programming language"), etc. There's nothing wrong with using this definition.

Meanwhile there's an alternate universe in a particular Zulip chat where "Lean" means specifically the core language and definitely not mathlib, and where there's a remarkable pile of ad-hoc excuses for the mountain of public exceptions and the lack of errata (it's not a mountain, these are isolated mistakes that are really hard to find, it's just an occasional slip from Kevin, okay it's not just Kevin but there's nothing from l’Académie française, this one was way back in 2019, that one was way back in 2022, the course really does teach people something about the language, etc.), and where a new paper writing "Lean's definition of fields" is engaging in academic misconduct.

Sorry, no, this doesn't survive Occam's razor. If you'd like to change terminology, start by clearly documenting the change and comprehensively updating other documentation to match; skip the fiction that people using the existing terminology are doing something wrong.

[Damiano Testa]

The existence of inconsistencies or imprecisions should not be an excuse to continue indulging in them, though.

[D. J. Bernstein]

Eric Wieser said:

That one is genuinely about Lean, induction is a builtin tactic, as are the natural numbers

For me this is further confirmation of the value of a name for the unified system (such as the established name, "Lean"). When I'm reporting properties that I observe from the system as a whole, I'm reporting what I know. I often don't know how these properties come from properties of the components---in this case, the core language versus mathlib---and I also don't want to pester the reader with irrelevant internal details.

[Arthur Paulino]

Maybe this is all a call to action. Apparently the leanprover-community needs some kind of official manifest clarifying all this from now on.

This is another personal impression of mine, which is aligned with a few other comments made on this thread: the structure of the Zulip server can strengthen such kinds of confusion. There exist Lean 4 and Mathlib. This is Zulip server is for Lean as a whole. And yet, threads about Mathlib are spread everywhere. In the #general stream, people talk about Mathlib and it's taken for granted that the thread is properly contextualized when, in fact, Mathlib is one (the major) Lean 4 library/use case.

Again, there's definitely history to explain the current scenario. But we need to acknowledge that this is very hard on newcomers and can backfire if we expect people to get the distinctions right.

[Rob Lewis]

I'm sorry this thread has gotten heated and I'd like to try to defuse some tension here. First of all,  there should be no accusation of academic misconduct here. Lean and mathlib are different entities, with different contributors, maintained by different organizations. Historically these lines have been very blurred, and this is reflected in a lot of the material on the web. It's not reasonable to expect someone new to the community to immediately grasp the current distinctions.

@D. J. Bernstein: I think most of the pushback in this thread is reactions to mathlib not being mentioned at all in your paper. Most of the people who have written the million lines of Lean code in mathlib see themselves as mathlib contributors, not Lean contributors. There are very few Lean contributors in comparison. Even though it clearly wasn't intentional, this reads as a mistaken attribution. Work that uses mathlib should mention that it is based on mathlib and cite the CPP 2020 paper by The Mathlib Community (and I mean "should" in the peer review suggestion sense, not as an accusation). Would you mind adding these to your paper? 

I agree with the opinions here that I personally would refer to "mathlib" instead of "Lean" at various points in your paper. I also think that, with a mention and reference to mathlib at the start, it's entirely clear what's meant and not a point worth arguing about. The semantics of Lean vs mathlib matter for development and could definitely stand to be clarified in places like the community website. (We're happy to take PRs from anyone updating unclear phrasing.) As a shorthand for "the context of your formalization" in your paper, write what you want.

[D. J. Bernstein]

Thanks for the comments.

Regarding your question, this was already answered much earlier, but I'll collect the quotes here for your convenience. Specifically, after a literature allusion appeared (with, I should note, wording that was neither clear nor temperate), I promptly wrote Poking around, I find DBLP:conf/cpp/X20, which of course I'm happy to cite and posted the following draft text: See \cite{1996/harrison} for an introduction to HOL Light, \cite{2021/moura} for an introduction to Lean 4, and \cite{2020/mathlib} for an introduction to the Lean math library. This appendix says ``HOL Light'' and ``Lean'' to refer to the full proof assistants available when these formalizations began, including the math libraries.

Regarding terminology for the unified system presented to users, at this point I've seen overwhelming evidence that "Lean" is the established name. This should be centrally documented in a way that's very easy to find (to be able to rapidly and conclusively terminate anything that's even remotely like the discussion that occurred above), and if different terminology is desired for whatever reason then that should be prominently documented as a change of terminology.

[Wrenna Robson]

Hi, @D. J. Bernstein. I know you and I have talked about this kind of thing before (and I spent some time trying to get that very paper formalised in Lean/Mathlib 3 last year, to some mixed success). Can I help at all? This is pretty much my direct area of interest.

[Wrenna Robson]

As it happens, in fact, in recent days I've been adapting your own control bits formalisation to Lean 4, using a partrial Lean 3 adapation I did a couple of years ago as a base, to good success. I don't think I'm that far from having a full proof of the construction, though I'm really at the technical point of it.

[Wrenna Robson]

Indeed, I think you may even be using my Hamming weight portion of the library that I wrote for this very purpose!

[Wrenna Robson]

Ah, perhaps not, I see you have your own definition of it. Just so you know, this exists. https://leanprover-community.github.io/mathlib4_docs/Mathlib/InformationTheory/Hamming.html

[D. J. Bernstein]

Third paragraph of my appendix is citing Section 4 of your paper "for a report of previous progress towards formalizing this paper's theorems in Lean"; I figured it was better for the reader to look at your description than to have me try to give more details. Regarding further work, what I want to see in the end is theorems saying things like "this x86 code computes CM.Decap", and obviously many things still need to be done to put that together.

[Wrenna Robson]

Oh, nice!

[Wrenna Robson]

Yes - there's a big big road ahead for that kind of thing. I am coming to the end of my funding now (and so am trying to drag together a thesis out of all the things I've done and thought, as one does), but suffice it to say I have a lot of thoughts about it and I'm really excited to see serious senior cryptographers like yourself getting involved in the Lean/mathlib world.

[Wrenna Robson]

For various reasons I've been out of the lean world for a bit. Good to be back in just to see you be here!

[Wrenna Robson]

This was the archive of much of what I did last year. A lot of what I ended up doing ended up back-ported into mathlib, though, I think: I tended towards a more "finding the right way to state and fit things together" approach, which is much (much) slower. https://github.com/linesthatinterlace/goppadecoding

[Wrenna Robson]

In particular, I think most of https://leanprover-community.github.io/mathlib_docs/linear_algebra/lagrange.html was rewritten as a result of that work.

[Wrenna Robson]

Sorry, let me link to the mathlib4 docs. In particular, Lagrange.interpolate (https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Lagrange.html#Lagrange.interpolate) is essentially your "interpolator" (https://cr.yp.to/2023/leangoppa-20230726/Goppadecoding/vanishing.lean.html), but with the advantage that by construction it has the linearity between the values at the nodes and the polynomial. (Also, the Mathlib definition is computable.)

[D. J. Bernstein]

Beyond Goppa decoding and control bits, I'm planning to formalize the necessary sorting-network proofs soon. There are then all sorts of smaller pieces needed such as Fangcheng-style row reduction. I've heard about two echelon-form projects for Lean, and maybe one or both of those has done algorithmic proofs. I wrote a row-reduction proof of linear dependence for lightgoppa with an eye towards proving algorithms later. For stating and proving theorems about software, HOL Light has models of x86 and ARM, including enough instructions to be useful; I don't know whether Lean does.

It can certainly be time-consuming to organize things for integration into a central library. Given the urgency of rolling out post-quantum software and the damage that can be done by bugs, I've been prioritizing getting things proven and deferring cleanup thoughts.

[Wrenna Robson]

I want to share one lesson I've learned (painfully), as someone who, while much less of a cryptographer than you, was at a similar point myself in the past: in general, when working with Mathlib in particular, it is always so much better to use the library rather than making new definitions from scratch. This is because of the understanding of definitions as a cost, for which the price must be paid in the API to use them (lemmas). Using preconstructed objects about which theorems exist mean we get the API for free.

[Wrenna Robson]

I don't see anything wrong with your prioritisation, to be clear - it is just a thought.

[Wrenna Robson]

A mistake I see a lot of formalisation stuff make in our neck of the woods (that is, by cryptographers, not really yourself) is to treat "having a list of formalised statements and definitions" as a good thing. But I think over time I've come to believe that it isn't - it is a mortgage on the future whose price must be paid in LoC.

[Wrenna Robson]

Incidentally, thanks to comments made by our own @Eric Wieser recently, I've re-interpreted the control bits algorithm as operating on binary bits of the numbers (in that each layer of the control bits network corresponds to conditional flipping of a progressively more sigificant bit, where the control bits are indexed by the residuum left when you remove that bit).

[Wrenna Robson]

It turns out to be a really nice and very functional interpretation which made things "click" in this context.

[Wrenna Robson]

I don't think Lean has much stating and proving theorems about software. I believe it to be possible (I have never done this), especially in lean 4, to compile Lean code itself to efficient C or assembly, I think possibly in a way that is provably correct or which at least only relies on the trusted core. So one approach would be to implement CMcE totally in Lean, in both an "efficient" way and a way which preserves the algebraic abstractions, prove the bridge between them, prove the algebraic things about the latter you want and compile the efficient code which has these functional and mathematical guarantees along with it.

[D. J. Bernstein]

My appendix notes that Lean already had theorems on direct interpolation (which predates Lagrange, btw). But the conventional statement isn't really the right statement! Goppa decoding is one way to see this: applying the statement to Goppa decoding means taking the usual denominators and multiplying to cancel them. Humans tend to be familiar with the conventional statement and in any case do the cancellation very quickly, but the right statement doesn't have any divisions in the statement and the proof, and doesn't require a field.

[Wrenna Robson]

The conventional statement of Lagrange? I think I know what you mean.

[Wrenna Robson]

Over time I've grown more and more pessimistic about the role of this kind of verification in effectively reducing bugs. I think the messy state of the start of the NIST PQ signatures process has shown that, uh, cryptographers are not immune to obvious bugs which break their schemes. Your own work in that regard has shown that, as you continue to bat away and drill down on the... less robust entries. What I used to be more optimistic about, and am now more pessimistic about, is the role of verification and formal methods in that process. As you say, there is a tension between a desire to produce verified code in a timely manner, and making it lie flat with other work. But one thing I'm trying to do at the moment is reason and think through what exactly any of this actually means for what ought to matter - the security that the cryptography produces.

[Wrenna Robson]

Right, yes, I've reminded myself now - yes I agree completely, in a sense that interpolation isn't what one really wants because you multiply it up. I have a feeling that the "thing multiplied up" is precisely Lagrange.nodal (https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Lagrange.html#Lagrange.nodal), which I define here as needing a field but I think iirc that is almost certainly incorrect/a product of not having quite enough time.

[Wrenna Robson]

It might be because outside of a field one has to worry about uniqueness? But I'm fairly sure field is far too strong. Anyway, yes, Lean had most of this stuff before - the previous formulations were just less useful for the stuff we'd need to do.

[Jireh Loreaux]

@Wrenna Robson, instead of copying and pasting, you can use the linkifier, like so: docs#Lagrange.nodal

[Wrenna Robson]

Oh, thank you - sorry.

[Jireh Loreaux]

(no need to be sorry, I just wanted to remind you of that convenience :smiley:)

[D. J. Bernstein]

Wrenna Robson said:

I don't think Lean has much stating and proving theorems about software. I believe it to be possible (I have never done this), especially in lean 4, to compile Lean code itself to efficient C or assembly, I think possibly in a way that is provably correct or which at least only relies on the trusted core. So one approach would be to implement CMcE totally in Lean, in both an "efficient" way and a way which preserves the algebraic abstractions, prove the bridge between them, prove the algebraic things about the latter you want and compile the efficient code which has these functional and mathematical guarantees along with it.

To the extent that users are asking for really fast cryptographic code, the code is produced by humans with a mix of assembly and vector instructions rather than by "optimizing" compilers; https://cr.yp.to/talks.html#2015.04.16 explains the basic reasons for this. That's true even without the constraint of "certifying" (proving) the compiler (or the weaker but sufficient constraint of "translation validation", meaning proving that _this_ code was correctly compiled). So people are instead working on directly verifying machine language (or, in some cases, assembly via Jasmin). Theorems in any case need an instruction-set definition, which is more than a little bit painful to write and validate for modern instruction sets.

[D. J. Bernstein]

Somewhat less painful, for the important case of unrollable code, is to use symbolic-execution tools (SAW, angr, Manticore) to convert low-level code into a simpler language without vectors, jumps, memory, etc. This relies on the tools to have been adequately validated but makes subsequent proofs easier---if the proof tools can handle sequences of (say) 100000 instructions.

[D. J. Bernstein]

Those tools don't magically escape the instruction-set difficulty; angr still doesn't support AVX-512, for example.

[D. J. Bernstein]

Wrenna Robson said:

Over time I've grown more and more pessimistic about the role of this kind of verification in effectively reducing bugs. I think the messy state of the start of the NIST PQ signatures process has shown that, uh, cryptographers are not immune to obvious bugs which break their schemes. Your own work in that regard has shown that, as you continue to bat away and drill down on the... less robust entries. What I used to be more optimistic about, and am now more pessimistic about, is the role of verification and formal methods in that process. As you say, there is a tension between a desire to produce verified code in a timely manner, and making it lie flat with other work. But one thing I'm trying to do at the moment is reason and think through what exactly any of this actually means for what ought to matter - the security that the cryptography produces.

Given that McEliece's system has maintained the same security exponent despite a long string of focused attack papers over 45 years, we _hope_ that the exponent is optimal (and, more importantly, that concrete parameters take about as long to break as we think). It'd then be terrible to have security lost because of algorithm bugs or software bugs, and certainly proof tools can help eliminate those bugs.

But, indeed, we don't have proofs of the security levels. I very much doubt that the asymptotic security levels are provable. A concrete security claim such as 2^256 (in a carefully defined model) is, if correct, also trivially "provable", but there's no reason to think that anyone will ever know a proof.

We don't even have something that sounds much wimpier, namely proofs of the performance of the _known_ attacks that we think are fastest among known attacks. See also https://cat.cr.yp.to/cryptattacktester-20230614.pdf#appendix.B for a survey of many years of similar proof gaps for factorization, discrete logs, and lattices. We don't even have proofs of the performance of something as easy as a sensibly optimized brute-force search against AES-128!

It's certainly conceivable that in the end we'll end up with verified software for a cryptosystem whose security level is much lower than we think it is. I gave a short talk at last month's Lean event (https://cr.yp.to/talks.html#2023.07.11) covering some ways that proofs help in applied cryptography and some ways that they don't.

[Wrenna Robson]

Sounds great, I'll try and check it out soon.

[Wrenna Robson]

I am aware - I can't remember the name, is it FiatCrypto - that there is some really nice "we assemble the assembly in verified ways so you don't have to" fast implementations out there. And there's been some work recently - some using Jasmin, yeah - that gives me some hope that fast cryptography can also mean verified cryptography.

It seems to me that what is missing is true will from applied cryptographers (other than people like yourself and a few others - but what I might call the average practitioner of street cryptography) in using these tools for the things that they are good for. I've attended HACS for the last two years and that's been really good but I'm always a bit like... OK but how can we get this usable by not-We.

One thing I will say about Lean and in particular the mathlib project: it has an amazing, active and helpful user community. It's really impossible to undersell how important that is I think. I've wrestled with quite a few tools that nominally ought to be the exact correct tool for the job - but they're a nightmare to use and if you hit a block you're sunk.

[Wrenna Robson]

And yes... security levels in cryptography are, let's be real, something of a dark art. At the very least I think one ought to be honest about how many assumptions one makes...

[Wrenna Robson]

I don't know if you ever get the thing where you read some provable security proof and you're like - OK but where's the beef, what's the moment you do the Clever Thing that isn't just symbol-manipulation or "well I'm going to assume this is hard".

[Wrenna Robson]

FYI @D. J. Bernstein, I have acted on your comment that of course the "multiplied up" polynomials of Lagrange interpolation do not need to be a field, and refactored the file accordingly. #6714.

If you have further comments or thoughts they would be welcome. I think I am probably going to submit a future patch to move these definitions and proofs into the Polynomial namespace, so there's certainly more refactoring to be done.

[Wrenna Robson]

If you have any theorems or definitions that have come from your goppa decoding work above that you think belong into Mathlib, I'm happy to help with that, as I'm a bit more familiar with the process and shaking off the rust.

[Wrenna Robson]

One thing we do not have in Mathlib currently is a satisfactory definition of a (linear) code. Obviously there's lots of concrete definitions one could choose, but choosing the "right" definition in Lean was frustrating past the point of usefulness. Please let me know if you have thoughts. Getting some coding theory into Mathlib would be a great future goal, and one that is compatible with some of the cryptographic aims. You might also want to join up with some of those people looking at more computational aspects and proofs, but I'm not best placed to talk about that.

[Bolton Bailey]

Yes, linear codes would be good to have. I started a PR in mathlib3 !3#16774, but did not finish it (perhaps it could be ported at some point). I thought it would be useful for my own crypto goals, but I think I got sidetracked, and in any case, I felt my inexperience in writing code that isn't necessarily tailored to a particular goal, but was meant to be more of a general purpose API.

[Wrenna Robson]

I seem to recall I spent a while trying to define a construction to give a nice API around finding minimum distances. Trying to remember what it was called.

[Eric Wieser]

docs#Set.infSep ?

[Wrenna Robson]

It was docs#Set.infsep

[Wrenna Robson]

That name is wrong, it should be InfSep or infSep, yeah.

[Wrenna Robson]

As I recall there's also some things that are true for when the distance is specifically integer-valued that I never quite got round to writing down (and then life happened, as it does).

[D. J. Bernstein]

I eliminated all coding-theory terminology from this paper's theorem statements, so maybe I'm not the best person to ask for advice on an API for general linear codes. :-) Most of the literature is about k-linear codes defined as k-subspaces of k^n, normally with k required to be finite. Often the literature is doing arithmetic on indices so it's helpful to pick an index set, and then {1,...,n} is traditional but {0,...,n-1} is a bit smoother because the indices are often polynomial exponents. Some of the literature is on non-linear codes, codes over more general rings, infinite-length codes, and metrics other than the Hamming metric. Sometimes definitions are general enough to include lattices.

[Wrenna Robson]

The natural thing in mathlib is 0 to n-1 because tuples of k are Fin n -> k, and Fin n is the subtype of Nat from 0 to n-1 with the modular arithmetic.

[Wrenna Robson]

And yes the annoyance has been that in a sense to incorporate all possible things one might mean by "a code" is an almost uselessly wide definition.

[Wrenna Robson]

I have a feeling that actually the thing that makes codes interesting is often the fact that their metrics are integer valued as much as anything... something about that gives a discreteness that gives rise to interesting properties. But I'm not a coding theorist!

[Wrenna Robson]

Why did you decide to eliminate coding theory references in the statements? Not that I think it was the wrong decision, I can see why you might, but I'm interested in your own thinking.

[D. J. Bernstein]

The theorems in the paper are aimed at readers who simply want to understand Goppa decoding and don't want to take a full coding-theory course. The main metrics are the time to read theorems (including the necessary definitions) and the time to read proofs. Being in a Goppa code has such a simple formula that defining and using a name for it, either as a predicate or as a set, ends up as a loss in both metrics; this is obvious for the proofs (which are continually working with the formula) but also true for the theorem statements. Code length and designed distance already have short formulas in this context. Minimum distance is mathematically more interesting but doesn't show up in any of the theorems.

[Wrenna Robson]

Designed distance?

[D. J. Bernstein]

That's 2t+1 in this paper. When there's a construction that outputs a code and a decoding algorithm that's guaranteed to decode any t errors, people talk about 2t+1 as the "designed distance" or "design distance" of the construction---or, sloppily, of the code. Obviously the minimum distance of the code is at least as large.

[Wrenna Robson]

Oh, that makes sense. I'm not sure I've seen the term but I see why you'd have it.

[Oisin McGuinness]

There is a new preprint on @D. J. Bernstein 's site, https://cr.yp.to/papers.html#pwccp, titled "Papers with computer-checked proofs" It is an extremely interesting detailed and candid account of his recent formalizations, in both HOL Light and Lean (with mathlib) of various results (including the Goppa code article discussed upstream).

I don't want to spoil it, but it is a paper that deserves to have a large audience. (Possibly too long for the rumored special issue(s) of the Bulletin of the AMS coming up?)

Here is the Abstract: "This report gives case studies supporting the hypothesis that it is often affordable for a paper presenting theorems to also include proofs that have been checked with today’s proof-checking software."

And a fun intro to one section: "I heard about proof-checking software last century, but my first project..."

If you don't have time to read the whole paper, the introduction (pages 1--6) is recommended to all.

[D. J. Bernstein]

Thanks for the kind words! I think what most mathematicians have heard about formalization amounts to "It's really painful" and so they don't even consider it, even when they're in what I think is a very common situation, namely that they could rapidly get their N pages of proofs formalized along with adding <2N pages of background material to proof-assistant libraries. I'm hoping that more papers quantifying formalization time can give further authors a better idea of what's possible.

[Kevin Buzzard]

Yes I think you're publically displaying data which there is a dearth of.

[Alex Kontorovich]

Just one comment on:

"in the words of 1991 de Bruijn [28], referees “need not bother about correctness and can concentrate on whether the paper is interesting and new”"

This was not my experience editing the Exp Math special issue; referees discovered a mistake in the way a key concept was formalized, and the formalization had to be redone!... See: https://www.tandfonline.com/doi/full/10.1080/10586458.2022.2088982

(Of course I agree that, once the definitions and statements have been carefully checked, the rest of the refereeing load is significantly reduced. But sometimes the definitions are the key new idea, and can be extremely complicated...)

[D. J. Bernstein]

Section 4.2 of my report focuses on risks of misformalizations. Countermeasures are previewed in Section 2.1, in various examples in Section 3, and in Section 4.1. Of course, even without computers, people often get definitions terribly wrong, whether the complications come from the depth of (some) pure mathematics or from the intrinsic complexity of (some) applications: for example, [72] surveys proof failures in cryptography, and many of the failures are convincingly attributed to bad definitions.

[D. J. Bernstein]

My reading of de Bruijn's article is that his concept of a referee evaluating whether the paper is "interesting" started with referees being given the formalized version of the paper, and his "lighten the burden" came from the referee not having to worry about whether the proofs are correct. I wouldn't interpret "lighten" as "eliminate".