Formalizing modern maths

Stream: maths

[Chris Hughes]

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⟩

[Patrick Massot]

People are crazy

[Patrick Massot]

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.

[Jesse Michael Han]

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

[Patrick Massot]

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.

[Rob Lewis]

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.

[Johan Commelin]

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/

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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