What's new in Lean 3

Stream: general

[Kyle Miller]

There have been a few Lean releases with new features, so I thought I'd give some abbreviated release notes. I'm skipping all the useful bug fixes and preparations for mathport, focusing instead on more visible changes. Mathlib is now on 3.42.0c.

Lean 3.42.0c

• fix for the "unknown declaration" error when rebuilding oleans involving private definitions
• add a noncomputable! modifier to completely inhibit VM compilation for definitions (replaces force_noncomputable)
• add check that non-Prop theorems be noncomputable (so Lean will tip you off that you're going against the mathlib def_lemma linter)

Lean 3.41.0c

• let sorry take an ignored tactic block, so sorry { ... } works to skip slow or incomplete subproofs
• add options for controlling numeral pretty printing. set_option pp.numeral_types true adds type ascriptions to numerals. This is also controlled by the pp_numeral_type attribute, for example attribute [pp_numeral_type] fin.
• make the noncomputability checker aware of computational irrelevance of parameters in constructors. (Now, for example, you can have computable instances for typeclasses with noncomputable parameters.)
• add a search engine for finding relevant lemmas, for applications such as using external automated provers. (lean#696)

Lean 3.39.0c

• add option pp.parens to cause the pretty printer to ignore precedence and print all parentheses

Lean 3.38.0c

• make simp only use all congr lemmas
• make simp not synthesize subsingleton instances, which introduce diamond issues
• add special support for congruence lemmas for decidable instances

Lean 3.37.0c

• improve simp's handling of out_param

[Kevin Buzzard]

Some experimentation seems to indicate that these features are all now available in mathlib right now -- am I right? This would be very cool because force_noncomputable is very popular in London. I see that mathlib's leanpkg.toml says lean_version = "leanprover-community/lean:3.42.0" but I'm a bit unsure about what the c means in Lean 3.42.0c.

[Kyle Miller]

I think that's the "c": leanprover-community/lean:3.42.0

[Kevin Buzzard]

Oh, c for community?

[Johan Commelin]

Right, it's a little marker to show that this is the forked version, not an MSR release.

[Kevin Buzzard]

I sometimes worry about what will happen when all these people who are populating the lean4 stream (and this is currently a really active stream, it's exciting to see) start saying "we want to use some of your mathlib stuff but not all of it so please start fragmenting". I remember pre-3.4.2 when the mathlib community were less in sync with the Lean developers and things were slightly more complicated. Since the fork the mathlib people and the Lean 3 people have been working together as one unit, essentially -- Kyle's post above is yet another example of this; many of these changes were inspired by mathlib. Right now we have got a super-efficient set-up, with development of difficult mathematics yielding subtle issues in core Lean (e.g. force_noncomputable) which are then fixed (e.g. with noncomputable!) and everyone is happy. Similarly there is a very smooth transition between the major developments which depend on mathlib (such as LTE) and mathlib itself, with the for_mathlib directories being ported when necessary. The Zulip makes this community super-smooth and functional. I am unclear about for how long we can live in this nirvana.

[Arthur Paulino]

I've seen myself in this situation of needing "just this little bit of Mathlib4" a few times. Sometimes I add Mathlib4 as a dependency and sometimes I just sorry out some theorems or state them as axioms.

I think Lean 4 (and Lake) will be powerful enough to download just enough of the dependencies. Right now, It's a bit weird to download thousands of files when the main code has just a handful of them.