Category Archives: number theory

Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge. Continue reading

Posted in number theory | Tagged , | 11 Comments

Teaching dependent type theory to 4 year olds via mathematics

What is the number before 0? Who cares! How do children model numbers? An experiment with type theory. Continue reading

Posted in computability, Learning Lean, number theory, Type theory | Tagged , , | 8 Comments

IMO 2019 Q1

Thoughts on doing an IMO problem in Lean Continue reading

Posted in General, number theory, Olympiad stuff | Tagged , , | 6 Comments

Column addition

Lean has two copies of basic number types such as the naturals or integers. The reason is that Lean users might want to do two completely different things with numbers such as these. Some people might want to prove theorems … Continue reading

Posted in Learning Lean, number theory | Leave a comment

617 is prime

More number theory today. Clara List and Sangwoo Jo were trying to do a question from the third year number theory example sheet; to work out whether 605 was a square modulo 617. They decided to assume the law of … Continue reading

Posted in number theory, tactics | 4 Comments

Quadratic Reciprocity and (p^2-1)/8

The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean! [edit March 2019; QR is now in Lean, thanks to Chris Hughes, but let’s not let that spoil the story.] Clara List and … Continue reading

Posted in Learning Lean, number theory | Leave a comment