Laurent Théry


  • Organisation: INRIA
  • Research Unit: Sophia Antipolis
  • Project: MARELLE
  • Address: 2004, route des Lucioles - B.P. 93 06902 Sophia Antipolis Cedex France
  • Phone: +33 4 92 38 76 87
  • Fax: +33 4 92 38 50 29
  • E-mail:
  • PGP
  • Ftp Area
  • Emily, Jeremy

    Some Publications

    Yves Bertot, Laurence Rideau, Laurent Théry Distant Decimals of π: Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation Journal of Automated Reasoning, Volume 61 Issue 1-4, June 2018

    Laurent Fuchs, Laurent Théry, Implementing Geometric Algebra Products with Binary Trees, Advances in Applied Clifford Algebras, 2014, Volume 24, Number 2, Page 589

    Laurent Fuchs, Laurent Théry: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. Automated Deduction in Geometry 2010.

    Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    : `A Modular Formalisation of Finite Group Theory' Research Report 6156.

    Laurent Théry and Guillaume Hanrot
    `Primality Proving with Elliptic Curve' Research Report 6155.

    Laurent Théry,
    `Proving the group law for elliptic curves formally' Technical Report 330.

    Laurence Rideau and Laurent Théry,
    `Formalising Sylow's theorems in Coq', Technical Report 327 .

    Laurent Théry,
    ` Simplifying Polynomial Expressions in a Proof Assistant', Research Report 5614 .

    More publications


    my android application TicTacToe TuTor that plays perfectly.

    my android application Peanoware that lets you build natural deduction trees.

    Proof certificates for geometry.

    Fourier A reflected version of Fourier-Motzkin elimination for Coq.

    Sudoku Solver: A certified solver for the Sudoku.

    CoqRubik: A certified solver for the Mini Rubik.

    CoqSos A port of John Harrison's Sum of Square tactic for Coq.

    CoqPrime: certifying prime numbers

    Propositional logic: an applet to build formulae, an applet to build natural deduction proofs.

    Cyp, a proof tool to colour proofs

    Aïoli, a toolkit for interactive symbolic applications.

    Figue, an incremental two-dimensional layout engine.

    Gbcoq, a certified implementation of Buchberger's algorithm.

    CtCaml, a programming environment for CamlLight.

    Chol, a proof environment for Hol


    A formalisation of the group law for elliptic curves (Edwards curve). It follows the following paper by Tom Hales.

    A formalisation of the Generalised Towers of Hanoi

    A new version of Buchberger's algorithm for Gröbner basis in Coq with Ssreflect .

    A little animation Hopscotch in Scratch of the name of my research team (Marelle).

    A Formal Proof that 2-Sat can be solved in linear time

    A Formal Proof of Kosaraju algorithm

    Hexadecimal digits of Π in Coq using the Plouffe formula

    Floating Point Numbers and Formal Proof : 4 lectures in Coq.

    A Formal Proof in Coq of the Robbins problem.

    A Formal Proof of Feit-Thompson theorem (completed on September 20, 2012).

    Formalising Geometric Algebra.

    A workshop on numbers and proofs in June 2006 in Paris.

    A formalization in the Coq theorem prover of a Sudoku solver: paper, Coq files.

    Some tactics to reason about inequalities in Coq.

    A bibliography on formalised mathematics.

    Some formalisations in the Coq prover.

    A course on formal methods (in italian)

    A course on Java and Esterel (in italian)

    “ The aim of science is not to open the door to infinite wisdom, but to set a limit to infinite error. ”
    Bertolt Brecht
    Laurent Théry