GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → math-comp → odd-order

math-comp / odd-order

Licence: other
The formal proof of the Odd Order Theorem

Programming Languages

Coq
218 projects

Labels

coqssreflectmathcompodd-order-theoremfeit-thompson-theorem

Projects that are alternatives of or similar to odd-order

multinomials
Multinomials for the Mathematical Components library.
Stars: ✭ 12 (-40%)
Mutual labels:  coq, ssreflect, mathcomp
Actuary
Formalization of the basic actuarial mathematics using Coq
Stars: ✭ 17 (-15%)
Mutual labels:  coq, ssreflect, mathcomp
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Stars: ✭ 41 (+105%)
Mutual labels:  coq, ssreflect, mathcomp
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (-25%)
Mutual labels:  coq, ssreflect, mathcomp
finmap
Finite sets, finite maps, multisets and generic sets
Stars: ✭ 45 (+125%)
Mutual labels:  coq, ssreflect, mathcomp
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (-5%)
Mutual labels:  coq, ssreflect, mathcomp
Abel
A proof of Abel-Ruffini theorem.
Stars: ✭ 26 (+30%)
Mutual labels:  coq, ssreflect, mathcomp
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (+210%)
Mutual labels:  coq, mathcomp
coqdocjs
Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]
Stars: ✭ 28 (+40%)
Mutual labels:  coq
coq-program-verification-template
Template project for program verification in Coq
Stars: ✭ 26 (+30%)
Mutual labels:  coq
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Stars: ✭ 38 (+90%)
Mutual labels:  coq
hs-to-coq
Convert Haskell source code to Coq source code.
Stars: ✭ 64 (+220%)
Mutual labels:  coq
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Stars: ✭ 84 (+320%)
Mutual labels:  coq
alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Stars: ✭ 20 (+0%)
Mutual labels:  coq
coq-tal
Formalization of Typed Assembly Language (TAL) in Coq
Stars: ✭ 15 (-25%)
Mutual labels:  coq
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Stars: ✭ 20 (+0%)
Mutual labels:  coq
fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-5%)
Mutual labels:  coq
fcsl-pcm
Partial Commutative Monoids
Stars: ✭ 20 (+0%)
Mutual labels:  coq
imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Stars: ✭ 15 (-25%)
Mutual labels:  coq
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Stars: ✭ 119 (+495%)
Mutual labels:  coq
View All Similar Projects ➔

CI

A formal proof of the Odd Order Theorem

The repository contains a formal verification of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Installation

If you already have OPAM installed (a fresh or up to date version of opam 2 is required):

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-odd-order
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].