# Zulip Chat Archive

## Stream: maths

### Topic: Formalizing modern maths

#### 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⟩

#### Patrick Massot (Sep 06 2019 at 16:16):

People are crazy

#### 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.

#### 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

#### 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.

#### 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.

#### 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/

#### 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

#### Mario Carneiro (Sep 06 2019 at 22:25):

`mv_polynomial`

before the removal of `decidable_eq`

is a pretty good real world typeclass maze

#### 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