Advertisements
Category Archives: number theory
IMO 2019 Q1
Someone sent me a link to this year’s IMO questions this afternoon at work, and the first one caught my eye because it looked like a relatively straightforward functional equation question: find all such that . I’ve seen enough of … Continue reading
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
