Eric Wieser

Maintainer for #leanprover's Mathlib, @numpy, and #cocotb. Roboticist. PhD.

[Eric Wieser @EricWieser]

@Someody42 @pianocktailiste Fun fact: Lean's runtime model has pretty much exactly the universal "call by pointer value" semantics that Python has, except that Lean pretends harder than the objects are immutable. Both use the trick of mutating constant objects when they know no one is looking!

[Eric Wieser @EricWieser]

@davidmbudden Which leads to two natural follow-ups:
1. Should your complaint be directed at Lean itself?
2. Where in mathlib could we have prominently documented this convention such that you would have discovered it not via Twitter?

[Eric Wieser @EricWieser]

@davidmbudden In practice mathlib is using the "periodic snapshot approach". The mathlib tag "v4.24.0" means "an arbitrary snapshot of mathlib that used Lean v4.24.0", which allows two downstream projects to easily agree on a version of mathlib to use once they agree on a Lean tool chain.

[Eric Wieser @EricWieser]

@m_hiyama This is not quite the full story; to reach the 7GB size in an empty project depending on mathlib, you have to either:
* Explicitly `import Mathlib`, rather than importing something more specific.
* Run `lake exe cache get` without arguments, which eagerly fetches all of mathlib.

[Eric Wieser @EricWieser]

@davidmbudden @AndresRata_ There is no version I know of in which way003 is not an error.

[Eric Wieser @EricWieser]

@davidmbudden @AndresRata_ Note that on Zulip we get a Lean project a week claiming to solve a millennium problem, and a fair fraction of these are "my LLM pretended to invoke the Lean compiler and says it succeeded". https://t.co/stOit9RLpV is our current canned response to these and similar cases.

[Eric Wieser @EricWieser]

@davidmbudden @AndresRata_ Maybe this was part of the bait, but: your example of code that proves false but compiles... doesn't actually compile in the three versions of Lean I tried. To give you the benefit of the doubt; what version _does_ it compile in?

[Eric Wieser @EricWieser]

@AndresRata_ @davidmbudden Do you mean "if your Lean proof doesn't compile we won't look at it" or "if your mathematical claim is not encoded into a Lean proof we won't look at it"?

[Eric Wieser @EricWieser]

@davidmbudden @ElliotGlazer @MathGuyWithAI @inductionheads What do you mean by "within a versioned release"? Do you mean that you were expecting semver semantics between 4.20.0 and 4.25.0? Or that you had two "different" versions of 4.25.0 somehow?

[Eric Wieser @EricWieser]

@davidmbudden @ElliotGlazer Why do you care about the web editor? Just publish the code from your local machine as a git repo, which already includes the metadata to pin to an exact version. Users without a Lean install can always open a GitHub codespace if they want to interact.

[Eric Wieser @EricWieser]

@davidmbudden The errors about E3 look suspiciously related to https://t.co/HZRL2TGsOT, which would be consistent with the version mismatch explanation in https://t.co/FdzaS6q6JX

[Eric Wieser @EricWieser]

@davidmbudden A trap you might have fallen into is not pinning a particular Lean and Mathlib version, especially if your system does not match the web editor it appears you're using. You should make sure you distribute your final Lean file(s) with a lakefile, lean-toolchain, and lake-manifest.

[Eric Wieser @EricWieser]

@davidmbudden A trap you might have fallen into is not pinning a particular Lean and Mathlib version, especially if your system does not match the web editor it appears you're using. You should make sure you distribute your final Lean file(s) with a lakefile, lean-toolchain, and lake-manifest.

[Eric Wieser @EricWieser]

@davidmbudden These "warning"s sure look like Lean rejecting your proofs to me; anything red is almost surely a real error.

[Eric Wieser @EricWieser]

@ElliotGlazer @JasonRute @leanprover SafeVerify checks that a theorem _statement_ in a student- or AI-provided solution file is really the same as the one in a reference input file (e.g. no redefining what + means). Lean4checker does not do this. I don't know if SafeVerify also performs the checking of lean4checker.

[Eric Wieser @EricWieser]

@ElliotGlazer @JasonRute @leanprover The purpose of lean4checker is to take code that has already been executed, and check that its output (the olean files) contain terms that are accepted by the typing rules of Lean. This does not execute any user-provided code (unless Lean.reduceBool allows such execution)

[Eric Wieser @EricWieser]

@JasonRute @ElliotGlazer @leanprover If you want to verify that the kernel really accepted something, you should use https://t.co/DEoVnaLoUv.

[Eric Wieser @EricWieser]

@JasonRute @ElliotGlazer @leanprover The lesson here is that the Lean command line is only a frontend to the rigorous checking of the kernel, and can be trivial configured to bypass it. There are much simpler ways to bypass sending the theorem to the kernel; you can hide your code in a comment!

[Eric Wieser @EricWieser]

@roses10k @ElliotGlazer Yes, `Lean.ofReduceBool` and `Lean.trustCompiler`.

[Eric Wieser @EricWieser]

@AnimaAnandkumar @JasonRute Is a list of those 162 theorems available somewhere? From the paper, it seems many of these come from MiniF2F (which humans deliberately avoid trying to prove) and MIL source (which would not be a tutorial if all the exercises came pre-solved!)