A machine-checked proof of the odd order theorem
From MaRDI portal
Recommendations
Cited in
(90)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Hammer for Coq: automation for dependent type theory
- Automating formalization by statistical and semantic parsing of mathematics
- Formalization of the Lindemann-Weierstrass theorem
- A formal proof in Coq of Lasalle's invariance principle
- Certifying standard and stratified Datalog inference engines in SSReflect
- Formal proof of a machine closed theorem in Coq
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Incorporating quotation and evaluation into Church's type theory
- Univalence as a principle of logic
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Foreword to the special focus on formal proofs for mathematics and computer science
- Towards the automatic mathematician
- Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
- Experiences from exporting major proof assistant libraries
- Liquid tensor experiment
- Formal verification of cP systems using Coq
- A library for formalization of linear error-correcting codes
- Classification of finite fields with applications
- Formalization of universal algebra in Agda
- Modelling algebraic structures and morphisms in ACL2
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- A fully automatic theorem prover with human-style output
- Deepalgebra -- an outline of a program
- Type theory and formalisation of mathematics
- From informal to formal proofs in Euclidean geometry
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Reliability of mathematical inference
- Congruence closure in intensional type theory
- Engineering mathematics: the odd order theorem proof
- Asynchronous processing of Coq documents: from the kernel up to the user interface
- Computational Complexity Via Finite Types
- Point-free, set-free concrete linear algebra
- Proof verification technology and elementary physics
- Mining the Archive of Formal Proofs
- Towards the formalization of fractional calculus in higher-order logic
- A Modular Formalisation of Finite Group Theory
- Computational logic: its origins and applications
- Certified Graph View Maintenance with Regular Datalog
- An introduction to univalent foundations for mathematicians
- Recycling proof patterns in Coq: case studies
- A formalization of properties of continuous functions on closed intervals
- An introduction to mechanized reasoning
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Validating Mathematical Structures
- Formalizing the Face Lattice of Polyhedra
- Mechanically certifying formula-based Noetherian induction reasoning
- Simple type theory is not too simple: Grothendieck's schemes without dependent types
- Formalizing Galois theory
- Proof auditing formalised mathematics
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Reshaping the metaphor of proof
- Modularity in mathematics
- Category-based co-generation of seminal concepts and results in algebra and number theory: containment-division and Goldbach rings
- Implementing type theory in higher order constraint logic programming
- A formal proof of the Kepler conjecture
- Mtac: a monad for typed tactic programming in Coq
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Mining state-based models from proof corpora
- Towards Knowledge Management for HOL Light
- Univalent categories and the Rezk completion
- Homotopy limits in type theory
- Measure construction by extension in dependent type theory with application to integration
- A formalised theorem in the partition calculus
- Formalising Mathematics in Simple Type Theory
- What is the point of computers? A question for pure mathematicians
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- The formal verification of the ctm approach to forcing
- Mathematizing as a virtuous practice: different narratives and their consequences for mathematics education and society
- Satisfiability modulo finite fields
- An experiment of a formal proof of an intermediate-level theorem in algebra
- Algorithm and abstraction in formal mathematics
- Chain Bounding, the Leanest Proof of Zorn’s Lemma, and an Illustration of Computerized Proof Formalization
- Mathematical structures in dependent type theory (invited talk)
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- A formal study of Boolean games with random formulas as payoff functions
- Exploring formal math on the blockchain: an explorer for Proofgold
- Towards solid abelian groups: a formal proof of Nöbeling's theorem
- Toward a geometry for syntax
- Formalizing factorization on Euclidean domains and abstract Euclidean algorithms
- Touring the MetaCoq project
- Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
- Formalization of algebraic theorems in PVS (invited talk)
- Automated reasoning for mathematics
- A Unified Framework for Formalizing Matrix Decomposition Proofs
- Formalising new mathematics in Isabelle: diagonal Ramsey
- A formalization of multi-tape Turing machines
- Computer-aided proof of Erdős discrepancy properties
This page was built for publication: A machine-checked proof of the odd order theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327343)
