Fermat, Euler, Wilson -- three case studies in number theory

DOI10.1007/s10817-016-9387-zzbMath1439.68027OpenAlexW2529619281MaRDI QIDQ1707601

Nathan Wasser, Christoph Walther

Publication date: 3 April 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9387-z

zbMATH Keywords

number theoryprogram verificationtheorem proving by induction

Mathematics Subject Classification ID

History of number theory (11-03) Congruences; primitive roots; residue systems (11A07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computer assisted proofs of proofs-by-exhaustion type (68V05)

Uses Software

• Isabelle
• NQTHM
• VeriFun
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• On proving the termination of algorithms by machine
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• Proof Checking the RSA Public Key Encryption Algorithm

This page was built for publication: Fermat, Euler, Wilson -- three case studies in number theory