Formal and efficient primality proofs by use of computer algebra oracles

DOI10.1006/jsco.2001.0457zbMath1044.03503OpenAlexW2031410477MaRDI QIDQ597112

Martijn Oostdijk, Olga Caprotti

Publication date: 6 August 2004

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.2001.0457

zbMATH Keywords

computer algebraPocklington criterionprimality of large positive numbers

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Cryptography (94A60) Mechanization of proofs and logical operations (03B35) Primality (11Y11)

Related Items (max. 100)

Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec ⋮ Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants ⋮ Verification of the Miller-Rabin probabilistic primality test. ⋮ Equality in computer algebra and beyond. ⋮ A certificate-based approach to formally verified approximations ⋮ View of Computer Algebra Data from Coq

Uses Software

• Coq
• Magma
• PARI/GP
• Theorema
• OMRS
• Automath
• Analytica

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
• A Skeptic's approach to combining HOL and Maple
• Integrating computer algebra into proof planning
• Towards the Mathematics Software Bus
• Autarkic computations in formal proofs
• On the role of OpenMath in interactive mathematical documents

This page was built for publication: Formal and efficient primality proofs by use of computer algebra oracles