Lean repository linked
One curious proof of Fermat's little theorem
arXiv:0801.0805 · arXiv
Lean formalisations (1)
seewoo5/DifferentProofs at 5093e4f59d6d
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.