Exercise
- Define Graham's number in your favorite proof assistant:
G : ℕ. - Prove
G > 0. - Prove that the last (least significant) digit of
Gis a 7:G % 10 == 7.
Let us collect solutions in this repository!
- a solution in Agda (using the standard library)
- a solution in Lean 4 (using mathlib)
- a partial solution in Coq
We are in particular waiting for solutions in Isabelle/HOL and HOL Light! ;-)