Zulip Chat Archive

Stream: general

Topic: Another week, another Lean


Gabriel Ebner (May 20 2020 at 09:53):

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 (May 20 2020 at 10:11):

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

Patrick Massot (May 20 2020 at 10:12):

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

Gabriel Ebner (May 20 2020 at 10:12):

Yes, please!

Patrick Massot (May 20 2020 at 10:14):

#2756

Patrick Massot (May 20 2020 at 10:26):

My computer says it works!

Patrick Massot (May 20 2020 at 10:46):

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

Kevin Buzzard (May 20 2020 at 11:52):

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 π3.14\pi\not=3.14.

Patrick Massot (May 20 2020 at 11:54):

It's not 3.143.14, it's 3.14.03.14.0

Johan Commelin (May 20 2020 at 12:16):

Thanks, Gabriel!

Jalex Stark (May 21 2020 at 02:00):

I think it's not possible to prove this:

example : π  3.14.0 := sorry

So we must be fine! :smiley:


Last updated: Dec 20 2023 at 11:08 UTC