Zulip Chat Archive

Stream: maths

Topic: Formalizing modern maths


view this post on Zulip Chris Hughes (Sep 06 2019 at 16:06):

Today I formalised a modern maths theorem

import tactic.norm_num

example :  a b c : , a^3 + b^3 + c^3 = 42 :=
⟨-80538738812075974, 80435758145817515, 12602123297335631, by norm_num

view this post on Zulip Patrick Massot (Sep 06 2019 at 16:16):

People are crazy

view this post on Zulip Patrick Massot (Sep 06 2019 at 16:24):

It makes me think we still haven't advertised the sensitivity formalization. We should really do that before people forget and this conjecture and get excited about 42 being a sum of three squares.

view this post on Zulip Jesse Michael Han (Sep 06 2019 at 16:35):

i think documenting our typeclass woes in the sensitivity conjecture could also be valuable

we could try to prepare a short paper for CPP 2020

view this post on Zulip Patrick Massot (Sep 06 2019 at 16:43):

Hmm, I'm currently writing a perfectoid spaces paper for CPP, and I would find it really unfair if our summer vacation beach project is worth a CPP paper. And what happened with type classes and coercions last summer is awful advertisement for Lean.

view this post on Zulip Rob Lewis (Sep 06 2019 at 17:27):

CPP doesn't have a "short paper" track and this project doesn't warrant a long paper. It seems more suitable for a blog post right now. Maybe a short paper at ITP next year, but that's a ways off.

view this post on Zulip Johan Commelin (Sep 06 2019 at 20:14):

Today I formalised a modern maths theorem

import tactic.norm_num

example :  a b c : , a^3 + b^3 + c^3 = 42 :=
⟨-80538738812075974, 80435758145817515, 12602123297335631, by norm_num

Relevant link: https://math.mit.edu/~drew/

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 21:43):

i think documenting our typeclass woes in the sensitivity conjecture could also be valuable

Leo says he is interested in abstract "typeclass mazes" where Lean 3 fails to infer typeclass efficiently. He has ideas for how the typeclass system should work in Lean 4 but wants to test his ideas on real world examples that come up in the wild

view this post on Zulip Mario Carneiro (Sep 06 2019 at 22:25):

mv_polynomial before the removal of decidable_eq is a pretty good real world typeclass maze

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 22:26):

What is an explicit example of a typeclass search problem which Lean 3 has trouble with?


Last updated: May 10 2021 at 08:14 UTC