Ex 1 Half done. Four sorrys left.
Ex 2 done
Ex 5 done
Ex 6 done
Ex 7 done (code is slow though)
Ex 1 : Two sorries left.
Ex 2 : Five sorries left.
Ex 3 : Two sorries left.
Ex 4 : Two sorries left.
Ex 5 : One sorry left.
Ex 6 : Statement formalised. Exercise: can we write down a beautifully-commented proof to make this solution a "model solution"?
Ex 7 : statement formalised
Ex 8 : done
No statements have been formalised here.
Ex 1 : done
No statements have been formalised here.
Ex 1 : done
2-4 : statement not formalised
5 : done
6 : have definition of Lucas sequence
7,8: statement not formalised
9: statement formalised; proof contains a sorry
No statements have been formalised here.
Ex 1 : done Ex 2 : done Ex 3 : part a, b done. Part c statment Ex 4 : done Ex 5 : done
Ex 7 : done
Ex 8 : done
Ex 9 : done
nothing formalised
Ex 1 done
2 statement formalised
3 done
4 statement formalised
5 statement not formalised
6 statement formalised
7 statement formalised
No statements have been formalised here
1 done 2 done 3 done 4 done 5 done 6 done 7 done 8 done
Nothing formalised
ex 1 parts a-c done, part d the statement is formalised but no proof
Q1-9 statements formalised, no proofs
Ex 1 parts i and ii done, iv to vi stated Ex 3,4 done Ex 5 parts a and b done. Ex 7 parts i to iii done
Ex 10 part a done, part b stated