Here’s what some of Imperial’s undergraduates have been doing.
I was told last year by an undergraduate that the official pdf solution I circulated to the students in 2016 was incomplete and the undergraduate did half-convince me of this. However I know for sure that Chris’ proof is complete, although philosophically there is still the issue of whether his formalisation of the problem is correct. This is an issue of interpretation rather than mathematics.
One of my first year tutees, Jin Su (Cris), told me the following great question: Let’s say I tell two of my tutees secret non-negative integers, and then I wrote two distinct non-negative integers on my whiteboard; one is the sum of the two secret integers, and the other one is not. I then take it in turns asking my tutees whether they know the other tutee’s number! Prove that eventually one of them will (truthfully) say “yes”.
I would imagine that this question can be dealt with in a similar manner. Mario Carneiro on the Lean gitter chat said that “usually knowledge is represented by a predicate of possible worlds rather than “things I know” ” . Can anyone (a) work out what he means and (b) reprove the Islanders problem using this approach or (c) solve Cris’ problem using any method at all?
Ellen Arlt proved that if R was a ring, then the set of n by n matrices over R was also a ring. Proving that inductive types have a complex structure (such as a ring structure) is harder than you might imagine; there were Lean issues which we had to solve. There were also mathematical issues which we had to solve; we had to learn how to manipulate finite sums (e.g. change order of summation), so we ended up learning a lot of generally useful skills. Ellen — please PR your work and I’ll link to it! A preliminary version is here but she finished the job yesterday. One thing that surprised me about the work was that she did not assume that the ring R was commutative! For sure it would be difficult to define the determinant of a matrix if the entries were in a non-commutative ring (even the case of a diagonal matrix is an issue). But the basic ring structure does not need commutativity of R, so I learnt something myself here.
Equivalence relations and congruences.
Julian Wykowski formalised several of the results which I proved in M1F about congruence of positive integers. In particular he proved that being congruent mod m was an equivalence relation, and various other important facts about congruences (such as how they behave well with respect to addition and multiplication). Julian’s work is here . It’s very clearly written; why not goof around with it online by following this link ?
The Exponential Function
Chris Hughes is formalising the exponential function and its basic properties, such as . This is very interesting to me because of all the theorems I proved in M1F, the de Moivre stuff is definitely the stuff that lies “furthest away from the axioms” and hence needs the most work.
Localisation of a ring.
Last but most definitely not least — Kenny Lau has formalised a sufficiently large amount of Atiyah–Macdonald’s book on commutative algebra to enable us to localise a commutative ring at a multiplicative set. We are now well on the way to defining affine schemes in Lean and once these are defined, defining a scheme in full generality should be not too much of a problem. Kenny’s work can be found here and in particular his localisation work is here although I believe it has just been accepted into mathlib! Well done Kenny!
Thank you to all students who have contributed recently.