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

DOI10.1007/S10817-016-9387-ZMaRDI QIDQ1707601zbMATH OpenOpenAlexFDO

Authors Christoph Walther, Nathan Wasser

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) Computer assisted proofs of proofs-by-exhaustion type (68V05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A String of Pearls: Proofs of Fermat's Little Theorem
• A string of pearls: proofs of Fermat's little theorem
• scientific article; zbMATH DE number 1795747
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• scientific article; zbMATH DE number 1391688

Cites work

• A theorem prover for a computational logic
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1795747 (Why is no real title available?)
• On proving the termination of algorithms by machine
• Proof Checking the RSA Public Key Encryption Algorithm

Cited in

(5)

• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• scientific article; zbMATH DE number 1795747 (Why is no real title available?)
• A string of pearls: proofs of Fermat's little theorem
• The arithmetics of Pierre Fermat in the context of the Mersenne correspondence: A microsocial approach
• On Fermat's and Euler's number-theoretical methods, their connections and their significance

Describes a project that uses

Uses Software

• Isabelle
• NQTHM
• VeriFun
• GitHub

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1707601)