Another week, another Lean

Stream: general

[Gabriel Ebner]

Good morning, everyone! It is this time of the week again. It fills me with joy to announce the latest release of the Lean community fork, Lean π! Obligatory excerpt from the changelog, this is a feature-only release:

Features:

• Coercions also trigger if the types have metavariables (lean#251)
• Better error message on missing imports (lean#253)
• Add add_eqn_lemma function (lean#254)

[Patrick Massot]

Am I right to be optimistic that porting mathlib should be pretty easy?

[Patrick Massot]

Should I simply open a PR that bumps the lean version and see if CI shares my optimism?

[Gabriel Ebner]

Yes, please!

[Patrick Massot]

#2756

[Patrick Massot]

My computer says it works!

[Patrick Massot]

See also #2758, especially for people who didn't understood what the above changelog was about.

[Kevin Buzzard]

I am slightly concerned that Lean $\pi$ is inconsistent. Using only tools in mathlib I am pretty confident that it is possible to prove that $\pi\not=3.14$.

[Patrick Massot]

It's not $3.14$, it's $3.14.0$

[Johan Commelin]

Thanks, Gabriel!

[Jalex Stark]

I think it's not possible to prove this:

example : π ≠ 3.14.0 := sorry

So we must be fine! :smiley: