pith. machine review for the scientific record. sign in

arxiv: 2604.20345 · v1 · submitted 2026-04-22 · 💻 cs.LO

Recognition: unknown

A Rocq Formalization of Simplicial Lagrange Finite Elements

CERMICS UMR 9032), Fran\c{c}ois Cl\'ement (SERENA, Houda Mouhcine (TOCCATA, LIPN, LIPN), Micaela Mayero (TOCCATA, SERENA, Sylvie Boldo (TOCCATA), Vincent Martin (LMAC)

Authors on Pith no claims yet

Pith reviewed 2026-05-09 23:27 UTC · model grok-4.3

classification 💻 cs.LO
keywords Rocqformal verificationfinite element methodLagrange elementsunisolvencesimplicialmultivariate polynomialsaffine spaces
0
0 comments X

The pith

The paper defines a finite element as a Rocq record and instantiates it with simplicial Lagrange elements of any dimension and degree, proving unisolvence.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper designs a finite element as a record in the Rocq proof assistant containing both the geometric and polynomial data and the proofs that these data satisfy the required properties. The key property is unisolvence, which ensures that the linear forms uniquely determine the polynomials. This formalization is then applied to the simplicial Lagrange finite elements with evenly distributed nodes, covering any dimension and any polynomial degree. A sympathetic reader would care because this step advances the long-term goal of proving the correctness of programs that use the finite element method to solve partial differential equations.

Core claim

A finite element is defined in Rocq as a record that includes the cell geometry, the polynomial approximation space, and a set of linear forms, together with proofs that the space has the correct dimension and that the forms are unisolvent. The record is instantiated with simplicial Lagrange finite elements for any dimension and degree, with the unisolvence proof included.

What carries the argument

The Rocq record for a finite element, which packages the cell vertices, the polynomial space, the degrees of freedom, and the validity proofs including unisolvence.

If this is right

  • The formal definition ensures that the Lagrange elements satisfy all mathematical requirements for any dimension and degree.
  • Supporting results on polynomials in finite and infinite-dimensional spaces are available as reusable Rocq components.
  • The unisolvence property is established even for the general case, which is noted as difficult.
  • This provides a basis for proving properties of finite element methods in a proof assistant.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This formalization advances the goal of proving correctness of scientific computing programs using the finite element method.
  • The lemmas developed can support formal proofs of other aspects of numerical analysis.
  • Generalization to non-simplicial elements or different node distributions would build directly on the record structure.
  • Once local cells are formalized, global mesh assembly and solution procedures become amenable to formal verification.

Load-bearing premise

The Rocq record definitions and supporting lemmas about polynomials and affine spaces accurately capture the intended mathematical concepts of finite elements.

What would settle it

For a specific simplex in dimension 2 with polynomial degree 1, the formalized linear forms would fail to be unisolvent if the proof does not establish that any polynomial vanishing on all nodes is the zero polynomial.

Figures

Figures reproduced from arXiv: 2604.20345 by CERMICS UMR 9032), Fran\c{c}ois Cl\'ement (SERENA, Houda Mouhcine (TOCCATA, LIPN, LIPN), Micaela Mayero (TOCCATA, SERENA, Sylvie Boldo (TOCCATA), Vincent Martin (LMAC).

Figure 1
Figure 1. Figure 1: 3D mesh of a cerebral aneurysm (colors only help to distinguish zones). [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Reference Lagrange finite elements LagP d k in dimension d = 2 (top) and d = 3 (bottom), with degrees of approximation k = 1 (left) and k = 2 (right). The geometric elements are d-simplices. The nodes (depicted by blue dots) are only the vertices when k = 1, and when k = 2, nodes are added in the middle of edges. Their coordinates being real numbers, they are denoted with a point suffix, such as in “0.” an… view at source ↗
Figure 3
Figure 3. Figure 3: Hierarchy of algebraic structures used in the present development. [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Affine geometric transformation T v in the case d = 2. Given v = (v0, v1, v2), T v maps the reference triangle Kˆ to the triangle K of vertices v. Given d+ 1 current vertices v of a current geometric element K ⊂ R d , an affine mapping send￾ing reference vertices vˆ onto v preserves barycenters (see the definition of aff_map in Section 5.1). Thus, the affine geometric transformation T v outputs the point w… view at source ↗
Figure 5
Figure 5. Figure 5: Injection onto a face hyperplane I v 0 in the case d = k = 3. The reference triangle Kˆ d−1 is first mapped onto the 0-th face of Kˆ d , opposite vertex vˆ0, and then to the 0-th face of Kd , that is contained in the face hyperplane Hv 0 supported by (v1, v2, v3). The hyperplanes are depicted in light blue and the faces in a darker blue. After reading Section 9.1 about nodes, note that the correspondence b… view at source ↗
Figure 6
Figure 6. Figure 6: Geometric transformation T τ 0 d (v) in the case d = k = 3. The transposition τ 0 d maps (0, 1, 2, 3) onto (3, 1, 2, 0). The reference simplex Kˆ d is mapped onto the current simplex K. The reference vertices are mapped onto the current vertices with a change of indices: for all i ∈ [0..d], we have T τ 0 d (v) (vˆi) = vτ 0 d (i) . Note that, as τ 0 d (d) = 0, the reference face hyperplane Hˆd (opposite ref… view at source ↗
Figure 7
Figure 7. Figure 7: Affine transformation of a finite element, from vertices to vertices. [PITH_FULL_IMAGE:figures/full_fig_p038_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Table of inputs and hypotheses for the finite element transformation [PITH_FULL_IMAGE:figures/full_fig_p038_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Lagrange nodes (aˆα)α∈Ad k of the reference simplex Kˆd when d ∈ {2, 3} and k = 3. Each node is depicted as a colored ball, and corresponds to a unique element of A d 3. The colors correspond to degrees l ⩽ 3 of polynomials, or equivalently to the sizes of multi-indices (i.e. in C d l for l ⩽ 3). In magenta, the node aˆ0 corresponds to constant polynomials (with degree 0) in P d 0, and to the multi-index 0… view at source ↗
Figure 10
Figure 10. Figure 10: Partition C d k = Uk i=0{(k − i, β)| β ∈ Cd−1 i }, with d = k = 3. Geometrically, {(k−i, β)| β ∈ Cd−1 i } is the intersection of the hyperplane of equation α0 = k−i (depicted in light pink) and of C d k (of equation α0 + α1 + α2 = k). The reference Lagrange node aˆ(α1,α2,α3) belonging to the face Hˆ0 is in blue and corresponds to the element (α1, α2, α3) ∈ Cd k. For instance, the set {(1, 2, 0),(1, 1, 1),… view at source ↗
Figure 11
Figure 11. Figure 11: Grsymlex ordering of A d k when d ∈ {2, 3} and k = 3. Dashed arrows represent the increase in the order. For A 2 3 (d = 2), we have (0, 0) < grsymlex (1, 0) < grsymlex (0, 1) < grsymlex (2, 0) < grsymlex (1, 1) < grsymlex (0, 2) < grsymlex (3, 0) < grsymlex (2, 1) < grsymlex (1, 2) < grsymlex (0, 3). When d ≥ 3, we have for instance for C 3 3 (3, 0, 0) < grsymlex (2, 1, 0) < grsymlex (2, 0, 1) < grsymlex … view at source ↗
Figure 12
Figure 12. Figure 12: Lagrange nodes of the reference simplex for [PITH_FULL_IMAGE:figures/full_fig_p048_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Passage from the reference subnodes of LagP 3 3 (degree ⩽ 3) to the reference nodes of LagP 3 2 (degree ⩽ 2) in the case d = k = 3. Plot of subvertices (vˆi )i∈[0..d] and subnodes (aˆα′ )α′∈A3 2 . The nodes (aˆα)α∈A3 3 are set in the tetrahedron defined by the vertices (vˆ0, vˆ1, vˆ2, vˆ3). The subvertices are (vˆ0, aˆ2δ0 , aˆ2δ1 , aˆ2δ2 ). The subnodes (aˆα′ )α′∈A3 2 are defined with respect to the tetra… view at source ↗
Figure 14
Figure 14. Figure 14: Various ways to equip R d with the affine space structure. Double-edged boxes denote actual instances of canonical structures in the Rocq system for R, that is to say possible terminal points for the canonical structure search. Rectangular boxes denote the intent to equip a space (either R or R d ) with an algebraic structure. Arrows correspond to generic canonical structures in our library, or in the Coq… view at source ↗
Figure 15
Figure 15. Figure 15: Dependency graph, including the literature (in green), our contributions presented in this [PITH_FULL_IMAGE:figures/full_fig_p059_15.png] view at source ↗
read the original abstract

Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finite element method, a popular method to numerically solve partial differential equations. In the long-term goal of proving its correctness, we focus here on the formal definition of what is a finite element. Mathematically, a finite element describes what happens in a cell of a mesh. It notably includes the geometry of the cell, the polynomial approximation space, and a finite set of linear forms that computationally characterizes the polynomials. Formally, we design a finite element as a record in the Rocq proof assistant with both values (such as the vertices of the cell) and proofs of validity (such as the dimension of the approximation space). The decisive validity proof is unisolvence, that makes the previous characterization unique. We then instantiate this record with the most popular and useful, the simplicial Lagrange finite elements for evenly distributed nodes, for any dimension and any polynomial degree, including the difficult unisolvence proof. These proofs require many results (definitions, lemmas, canonical structures) about finite families, affine spaces, multivariate polynomials, in the context of finite or infinite-dimensional spaces.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents a formalization in the Rocq proof assistant of finite elements as records containing geometric data, polynomial approximation spaces, and degrees of freedom with associated validity proofs, including the crucial unisolvence property. It specializes this to simplicial Lagrange finite elements with evenly distributed nodes, providing the construction and unisolvence proof for arbitrary dimensions and polynomial degrees, along with supporting mathematical libraries for finite families, affine spaces, and multivariate polynomials.

Significance. If the formalization is correct, this work is significant as it provides a machine-checked foundation for the finite element method, which is essential for proving the correctness of numerical solvers for PDEs. The generality to any dimension and degree, with the difficult unisolvence proof, is a notable achievement that can serve as a basis for further formal developments in scientific computing. The explicit machine-checked proofs and reusable library on polynomials and affine spaces are particular strengths.

major comments (1)
  1. The central claim is the instantiation of the finite-element record with a complete unisolvence proof for simplicial Lagrange elements of arbitrary dimension and degree. However, the manuscript describes the record structure and supporting lemmas at a high level without exhibiting the Rocq definition of the record type, the statement of the unisolvence lemma, or key intermediate results on the polynomial space dimension, leaving the load-bearing formalization unverifiable from the text.
minor comments (2)
  1. The abstract and introduction mention 'many results (definitions, lemmas, canonical structures)' on finite families and multivariate polynomials; a dedicated section or appendix listing the most important ones with their Rocq names would improve readability and reusability.
  2. Notation for affine spaces and evenly distributed nodes is introduced without a small concrete example (e.g., the 2D degree-1 or degree-2 case) that would help readers map the general construction to familiar finite-element tables.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their positive evaluation of the significance of our Rocq formalization and for the constructive feedback. We address the single major comment below.

read point-by-point responses

  1. Referee: The central claim is the instantiation of the finite-element record with a complete unisolvence proof for simplicial Lagrange elements of arbitrary dimension and degree. However, the manuscript describes the record structure and supporting lemmas at a high level without exhibiting the Rocq definition of the record type, the statement of the unisolvence lemma, or key intermediate results on the polynomial space dimension, leaving the load-bearing formalization unverifiable from the text.

    Authors: We agree that the manuscript presents the finite-element record and unisolvence proof at a high level. To improve direct verifiability of the central claim, the revised version will include the Rocq definition of the finite element record type, the precise statement of the unisolvence lemma, and key intermediate results establishing the dimension of the polynomial approximation space (including the cardinality of the chosen basis). These will be placed in a dedicated section or appendix, while preserving readability of the main text. The complete development with all proofs is already available in the public Rocq repository linked from the paper. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified.

full rationale

The paper presents a direct Rocq formalization of the standard mathematical definition of a finite element (as a record containing cell geometry, polynomial space, and degrees of freedom together with validity proofs including unisolvence). It instantiates this record for simplicial Lagrange elements of arbitrary dimension and degree using supporting libraries for affine spaces, multivariate polynomials, and finite families. No step reduces a claimed result to its own inputs by definition, no fitted parameters are renamed as predictions, and no load-bearing premise relies on a self-citation chain whose content is unverified outside the present work. The derivation is therefore self-contained as a faithful encoding of externally established mathematics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard mathematical results about polynomials and affine spaces from Rocq libraries without introducing new free parameters or invented entities.

axioms (1)
  • standard math Properties of finite families, affine spaces, and multivariate polynomials
    Used to construct the finite element record and prove unisolvence for general cases.

pith-pipeline@v0.9.0 · 5565 in / 1183 out tokens · 55017 ms · 2026-05-09T23:27:26.312671+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

57 extracted references · 34 canonical work pages · 1 internal anchor

  1. [1]

    Classical analysis with Coq

    Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub. Classical analysis with Coq. The 9th Coq Workshop, 2018. URL https://easychair.org/ smart-slide/slide/n3pK

    2018

  2. [2]

    Competing inheritance paths in dependent type theory: A case study in functional analysis

    Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: A case study in functional analysis. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Proc. of the 10th Internat. Joint Conf. on Automated Reasoning (IJCAR 2020) , volume 12167 of LNCS, pa...

    work page doi:10.1007/978-3-030-51054-1 2020

  3. [3]

    12 Black-hole perturbation theory,

    Ivo Babuˇ ska and Theofanis Strouboulis. The finite element method and its reliability . Nu- merical Mathematics and Scientific Computation. The Clarendon Press, Oxford University Press, New York, 2001. URL https://doi.org/10.1093/oso/9780198502760.001.0001

    work page doi:10.1093/oso/9780198502760.001.0001 2001

  4. [4]

    Ivo Babuˇ ska and J. Osborn. Eigenvalue problems. In Finite Element Methods (Part 1) , volume 2 of Handbook of Numerical Analysis , pages 641–787. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80042-0

    work page doi:10.1016/s1570-8659(05)80042-0 1991

  5. [5]

    Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs

    Yves Bertot. Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs. In Bernd Fischer and Tarmo Uustalu, editors, Proc. of the 15th Internat. Colloquium on Theoretical Aspects of Computing (ICTAC 2018), pages 3–10, Cham,

    2018

  6. [6]

    URL https://doi.org/10.1007/978-3-030-02508-3 1

    Springer. URL https://doi.org/10.1007/978-3-030-02508-3 1

    work page doi:10.1007/978-3-030-02508-3

  7. [7]

    Flocq: A unified library for proving floating-point algorithms in Coq

    Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Proc. of the IEEE 20th Symposium on Computer Arithmetic (ARITH 2020), pages 243–252, Los Alamitos, 2011. IEEE. URL https://doi.org/10.1109/ARITH.2011. 40

    work page doi:10.1109/arith.2011 2020

  8. [8]

    Wave equation numerical resolution: A comprehensive mech- anized proof of a C program

    Sylvie Boldo, Fran¸ cois Cl´ ement, Jean-Christophe Filliˆ atre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: A comprehensive mech- anized proof of a C program. J. Autom. Reason. , 50(4):423–456, 2013. URL https: //doi.org/10.1007/s10817-012-9255-4

    work page doi:10.1007/s10817-012-9255-4 2013

  9. [9]

    Coquelicot: A user-friendly library of real analysis for Coq

    Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci. , 9(1):41–62, 2015. URL https://doi.org/10. 1007/s11786-014-0181-1

    2015

  10. [10]

    A Coq formal proof of the Lax–Milgram theorem

    Sylvie Boldo, Fran¸ cois Cl´ ement, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax–Milgram theorem. InProc. of the 6th ACM SIGPLAN Internat. Conf. on Certified Programs and Proofs (CPP 2017), pages 79–89, New York, 2017. Association for Computing Machinery. URL https://doi.org/10.1145/3018610.3018625

    work page doi:10.1145/3018610.3018625 2017

  11. [11]

    A Coq formalization of Lebesgue integration of nonnegative functions

    Sylvie Boldo, Fran¸ cois Cl´ ement, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. J. Autom. Reason. , 66 (2):175–213, 2022. URL https://doi.org/10.1007/s10817-021-09612-0

    work page doi:10.1007/s10817-021-09612-0 2022

  12. [12]

    A Coq formalization of the Bochner in- tegral

    Sylvie Boldo, Fran¸ cois Cl´ ement, and Louise Leclerc. A Coq formalization of the Bochner in- tegral. Research Report RR-9456, Inria, 2022. URL https://inria.hal.science/hal-03516749/

    2022

  13. [13]

    A Coq formalization of Lebesgue induction principle and Tonelli’s theorem

    Sylvie Boldo, Fran¸ cois Cl´ ement, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli’s theorem. In M. Chechik, JP. Katoen, and M. Leucker, editors, Proc. of the 25th Internat. Symp. on Formal Methods (FM 2023), volume 14000 of LNCS, pages 39–55, Cham, 2023. Springer. URL https://doi.org/10...

    2023

  14. [14]

    Teaching divisibility and binomials with Coq

    Sylvie Boldo, Fran¸ cois Cl´ ement, David Hamelin, Micaela Mayero, and Pierre Rousselin. Teaching divisibility and binomials with Coq. In Julien Narboux, Walther Neuper, and Pedro Quaresma, editors, Proc. of the 13th Internat. Workshop on Theorem proving compo- nents for Educational software (ThEdu 2024) , volume 419 of EPTCS, pages 124–139, 2024. URL htt...

    work page doi:10.48550/arxiv.2404.12676 2024

  15. [15]

    Brenner and L.R

    Suzanne C. Brenner and L. Ridgway Scott. The Mathematical Theory of Finite Element Methods, volume 15 of Texts in Applied Mathematics. Springer, New York, 3rd edition, 2008. URL https://doi.org/10.1007/978-0-387-75934-0

    work page doi:10.1007/978-0-387-75934-0 2008

  16. [16]

    Collection Math´ ematiques Appliqu´ ees pour la Maˆ ıtrise

    Ha¨ ım Brezis.Analyse fonctionnelle. Collection Math´ ematiques Appliqu´ ees pour la Maˆ ıtrise. [Collection of Applied Mathematics for the Master’s Degree]. Masson, Paris, 1983. URL https: //www.dunod.com/sciences-techniques/analyse-fonctionnelle-theorie-et-applications-0. In French. Inria A Rocq Formalization of Simplicial Lagrange Finite Elements 63

    1983

  17. [17]

    P. G. Ciarlet and P. A. Raviart. General Lagrange and Hermite interpolation in Rn with applications to finite element methods. Arch. Ration. Mech. Anal. , 46(4):177–199, 1972. URL https://doi.org/10.1007/BF00252458

    work page doi:10.1007/bf00252458 1972

  18. [18]

    Philippe G. Ciarlet. Basic error estimates for elliptic problems. In Finite Element Meth- ods (Part 1) , volume 2 of Handbook of Numerical Analysis , pages 17–351. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80039-0

    work page doi:10.1016/s1570-8659(05)80039-0 1991

  19. [19]

    Philippe G. Ciarlet. The Finite Element Method for Elliptic Problems, volume 40 ofClassics in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM), Philadelphia,

  20. [20]

    The Finite Element Method for Elliptic Problems

    URL https://doi.org/10.1137/1.9780898719208. Reprint of the 1978 original [North- Holland, Amsterdam]

    work page doi:10.1137/1.9780898719208 1978

  21. [21]

    Finite element method

    Fran¸ cois Cl´ ement and Vincent Martin. Finite element method. Detailed proofs to be for- malized in Coq. Research Report RR-9557, Inria, 2024. URL https://inria.hal.science/ hal-04713897/. Release 1.0 (v1)

    2024

  22. [22]

    Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi

    Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi. In Zena M. Ariola, editor, Proc. of the 5th Internat. Conf. on Formal Structures for Computation and Deduction (FSCD 2020) , volume 167 of LIPIcs, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik. URL https: /...

    work page doi:10.4230/lipics.fscd.2020.34 2020

  23. [23]

    Cox, John Little, and Donal O’Shea

    David A. Cox, John Little, and Donal O’Shea. Ideals, Varieties, and Algorithms . Un- dergraduate Texts in Mathematics. Springer, Cham, 2015. URL https://doi.org/10.1007/ 978-3-319-16721-3

    2015

  24. [24]

    The Lean theorem prover (system description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Proc. of the 25th Internat. Conf. on Automated Deduction (CADE 2015) , vol- ume 9195 of LNCS, pages 378–388, Cham, 2015. Springer. URL https://doi.org/10.1007/ 978-3-319-21401-6 26

    2015

  25. [25]

    On the formalization of the heat conduction problem in HOL

    Elif Deniz, Adnan Rashid, Osman Hasan, and Sofi` ene Tahar. On the formalization of the heat conduction problem in HOL. In Kevin Buzzard and Temur Kutsia, editors, Proc. of the 15th Internat. Conf. on Intelligent Computer Mathematics (CICM 2022) , volume 13467 of LNCS, pages 21–37, Cham, 2022. Springer. URL https://doi.org/10.48550/arXiv.2208.06642

    work page doi:10.48550/arxiv.2208.06642 2022

  26. [26]

    Formal study of plane Delaunay triangulation

    Jean-Fran¸ cois Dufourd and Yves Bertot. Formal study of plane Delaunay triangulation. In Matt Kaufmann and Lawrence C. Paulson, editors, Proc. of the 1st Internat. Conf. on Interactive Theorem Proving (ITP 2010), pages 211–226, Berlin - Heidelberg, 2010. Springer. URL https://doi.org/10.1007/978-3-642-14052-5 16

    work page doi:10.1007/978-3-642-14052-5 2010

  27. [27]

    Theory and Practice of Finite Elements , volume 159 of Applied Mathematical Sciences

    Alexandre Ern and Jean-Luc Guermond. Theory and Practice of Finite Elements , volume 159 of Applied Mathematical Sciences. Springer, New York, 2004. URL https://doi.org/10. 1007/978-1-4757-4355-5

    2004

  28. [28]

    Finite Elements I

    Alexandre Ern and Jean-Luc Guermond. Finite Elements I. Approximation and Interpolation, volume 72 of Texts in Applied Mathematics. Springer, Cham, 2021. URL https://doi.org/10. 1007/978-3-030-56341-7

    2021

  29. [29]

    Finite Elements II

    Alexandre Ern and Jean-Luc Guermond. Finite Elements II. Galerkin Approximation, Elliptic and Mixed PDEs , volume 73 of Texts in Applied Mathematics . Springer, Cham, 2021. URL https://doi.org/10.1007/978-3-030-56923-5

    work page doi:10.1007/978-3-030-56923-5 2021

  30. [30]

    Finite Elements III

    Alexandre Ern and Jean-Luc Guermond. Finite Elements III. First-Order and Time- Dependent PDEs, volume 74 of Texts in Applied Mathematics . Springer, Cham, 2021. URL https://doi.org/10.1007/978-3-030-57348-5. RR n° 9590 64 S. Boldo, F. Cl´ ement, V. Martin, M. Mayero, H. Mouhcine

    work page doi:10.1007/978-3-030-57348-5 2021

  31. [31]

    Fernandes and P.A.F

    J.L.M. Fernandes and P.A.F. Martins. All-hexahedral remeshing for the finite element analysis of metal forming processes. Finite. Elem. Anal. Des. , 43(8):666–679, 2007. ISSN 0168-874X. URL https://doi.org/10.1016/j.finel.2007.02.001

    work page doi:10.1016/j.finel.2007.02.001 2007

  32. [32]

    Fern´ andez, Jean-Fr´ ed´ eric Gerbeau, and Vincent Martin

    Miguel A. Fern´ andez, Jean-Fr´ ed´ eric Gerbeau, and Vincent Martin. Numerical simulation of blood flows through a porous interface. M2AN Math. Model. Numer. Anal. , 42(6):961–990,

  33. [33]

    URL https://doi.org/10.1051/m2an:2008031

    work page doi:10.1051/m2an:2008031

  34. [34]

    Fujita and T

    Hiroshi Fujita and Takashi Suzuki. Evolution problems. In Finite Element Methods (Part 1), volume 2 of Handbook of Numerical Analysis , pages 789–928. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80043-2

    work page doi:10.1016/s1570-8659(05)80043-2 1991

  35. [35]

    Constructive reals in Coq: Axioms and categoricity

    Herman Geuvers and Milad Niqui. Constructive reals in Coq: Axioms and categoricity. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Proc. of the Internat. Workshop on Types for Proofs and Programs (TYPES 2000) , volume 2277 of LNCS, pages 79–95, Berlin - Heidelberg, 2002. Springer. URL https://doi.org/10.1007/ 3-540-45842-5 6

    2000

  36. [36]

    A small scale reflection extension for the Coq system

    Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A small scale reflection extension for the Coq system. Research Report RR-6455, Inria, 2008. URL https://inria.hal.science/ inria-00258384/

    2008

  37. [37]

    Cours de math´ ematiques sp´ eciales - 1

    Bernard Gostiaux. Cours de math´ ematiques sp´ eciales - 1. Alg` ebre [Lecture Notes in Special Mathematics - 1. Algebra] . Math´ ematiques. Presses Universitaires de France, Paris, 1993. URL https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre. In French

    1993

  38. [38]

    Cours de math´ ematiques sp´ eciales - 4

    Bernard Gostiaux. Cours de math´ ematiques sp´ eciales - 4. G´ eom´ etrie affine et m´ etrique [Lecture Notes in Special Mathematics - 4. Affine and metric geometry] . Math´ ematiques. Presses Universitaires de France, Paris, 1995. URL https://www.puf.com/ cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique. In French

    1995

  39. [39]

    Numerical analysis of ordinary differential equations in Isabelle/HOL

    Fabian Immler and Johannes H¨ olzl. Numerical analysis of ordinary differential equations in Isabelle/HOL. In Lennart Beringer and Amy P. Felty, editors,Proc. of the 3rd Internat. Conf. on Interactive Theorem Proving (ITP 2012) , volume 7406 of LNCS, pages 377–392, Berlin - Heidelberg, 2012. Springer. URL https://doi.org/10.1007/978-3-642-32347-8 26

    work page doi:10.1007/978-3-642-32347-8 2012

  40. [40]

    Mathematical aspects of variational boundary integral equations for time dependent wave propagation

    Patrick Joly and Jer´ onimo Rodr´ ıguez. Mathematical aspects of variational boundary integral equations for time dependent wave propagation. J. Integral Equ. Appl. , 29(1):137–187, 2016. URL https://doi.org/10.1216/JIE-2017-29-1-137

    work page doi:10.1216/jie-2017-29-1-137 2016

  41. [41]

    chinchilla optimal

    Marie Kerjean, Micaela Mayero, and Pierre Rousselin. Maths with Coq in L1, a pedagogical experiment. In Julien Narboux, Walther Neuper, and Pedro Quaresma, editors, Proc. of the 13th Internat. Workshop on Theorem proving components for Educational software (ThEdu 2024), volume 419 of EPTCS, pages 112–123, 2024. URL https://doi.org/10.48550/arXiv. 2505.05990

    work page internal anchor Pith review doi:10.48550/arxiv 2024

  42. [42]

    doi: 10.1007/978-3-642-39634-2\_14.https://inria.hal.science/hal-00816699

    Assia Mahboubi and Enrico Tassi. Canonical structures for the working Coq user. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Proc. of the 4th Internat. Conf. on Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pages 19–34, Berlin - Heidelberg, 2013. Springer. URL https://doi.org/10.1007/978-3-642-39634-2 5

    work page doi:10.1007/978-3-642-39634-2 2013

  43. [43]

    Mathematical Components

    Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, Gen` eve, 2020. URL https://doi.org/10.5281/zenodo.7118596

    work page doi:10.5281/zenodo.7118596 2020

  44. [44]

    Vincent Martin, J´ erˆ ome Jaffr´ e, and Jean E. Roberts. Modeling fractures and barriers as interfaces for flow in porous media. SIAM J. Sci. Comput. , 26(5):1667–1691, 2005. URL https://doi.org/10.1137/S1064827503429363. Inria A Rocq Formalization of Simplicial Lagrange Finite Elements 65

    work page doi:10.1137/s1064827503429363 2005

  45. [45]

    Formalisation et automatisation de preuves en analyses r´ eelle et num´ erique [Formalization and Proof Automation in Real and Numerical Analysis]

    Micaela Mayero. Formalisation et automatisation de preuves en analyses r´ eelle et num´ erique [Formalization and Proof Automation in Real and Numerical Analysis] . Th` ese de Doc- torat, Universit´ e Paris VI, 2001. URL https://www-lipn.univ-paris13.fr/%7Emayero/publis/ these-mayero.ps.gz. In French

    2001

  46. [46]

    Automation for geometry in Isabelle/HOL

    Laura Meikle and Jacques Fleuriot. Automation for geometry in Isabelle/HOL. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors, Proc. of the 2nd Workshop on Practical Aspects of Automated Reasoning (PAAR 2010), volume 9 of EPiC Series in Computing, pages 84–94, Bramhall, UK, 2012. EasyChair. URL https://doi.org/10.29007/r5k7

    work page doi:10.29007/r5k7 2010

  47. [47]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS. Springer, Berlin - Heidelberg, 2002. URL https://doi.org/10.1007/3-540-45949-9

    work page doi:10.1007/3-540-45949-9 2002

  48. [48]

    Kawamoto, and Hiroshi Yamazaki

    Sora Otsuki, Pauline N. Kawamoto, and Hiroshi Yamazaki. A simple example for linear partial differential equations and its solution using the method of separation of variables. Formaliz. Math., 27(1):25–34, 2019. URL https://doi.org/10.2478/forma-2019-0003

    work page doi:10.2478/forma-2019-0003 2019

  49. [49]

    D´ efinitions Inductives en Th´ eorie des Types [Inductive Definitions in Type Theory]

    Christine Paulin-Mohring. D´ efinitions Inductives en Th´ eorie des Types [Inductive Definitions in Type Theory]. Habilitation ` a diriger les recherches, Universit´ e Claude Bernard Lyon I, 1996. URL https://hal.science/tel-00431817/. In French

    1996

  50. [50]

    Numerical approximation of partial differential equations, volume 23 of Springer Series in Computational Mathematics

    Alfio Quarteroni and Alberto Valli. Numerical approximation of partial differential equations, volume 23 of Springer Series in Computational Mathematics . Springer, Berlin - Heidelberg,

  51. [51]

    URL https://doi.org/10.1007/978-3-540-85268-1

    work page doi:10.1007/978-3-540-85268-1

  52. [52]

    Roberts and Jean-Marie Thomas

    Jean E. Roberts and Jean-Marie Thomas. Mixed and hybrid methods. In Finite Element Methods (Part 1) , volume 2 of Handbook of Numerical Analysis , pages 523–639. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05) 80041-9

    work page doi:10.1016/s1570-8659(05 1991

  53. [53]

    Nombres r´ eels dans Coq [Real numbers in Coq]

    Vincent Semeria. Nombres r´ eels dans Coq [Real numbers in Coq]. In Zaynah Dargaye and Yann Regis-Gianas, editors, Actes des 31es Journ´ ees Francophones des Langages Applicatifs (JFLA 2020) , pages 104–111. IRIF, 2020. URL https://inria.hal.science/hal-02427360/. In French

    2020

  54. [54]

    A formal proof of the Lax equivalence theorem for finite difference schemes

    Mohit Tekriwal, Karthik Duraisamy, and Jean-Baptiste Jeannin. A formal proof of the Lax equivalence theorem for finite difference schemes. In A. Dutle, M.M. Moscato, L. Titolo, C.A. Mu˜ noz, and I. Perez, editors,Proc. of the 13th Internat. Symp. NASA Formal Methods (NFM 2021), volume 12673 of LNCS, Cham, 2021. Springer. URL https://doi.org/10.1007/ 978-3...

    2021

  55. [55]

    Lars B. Wahlbin. Local behavior in finite element methods. In Finite Element Methods (Part 1), volume 2 of Handbook of Numerical Analysis , pages 353–522. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80040-7

    work page doi:10.1016/s1570-8659(05)80040-7 1991

  56. [56]

    Une th´ eorie des constructions inductives [A Theory of Inductive Con- structions]

    Benjamin Werner. Une th´ eorie des constructions inductives [A Theory of Inductive Con- structions]. Th` ese de Doctorat, Universit´ e Paris VII, 1994. URL https://hal.science/ tel-00196524v2. In French

    1994

  57. [57]

    O. C. Zienkiewicz, R. L. Taylor, and J. Z. Zhu. The Finite Element Method: its Basis and Fundamentals. Elsevier/Butterworth Heinemann, Amsterdam, 7th edition, 2013. URL https://doi.org/10.1016/B978-1-85617-633-0.00001-0. RR n° 9590 RESEARCH CENTRE Centre Inria de Saclay Bâtiment Alan T uring Campus de l’École Polytechnique 1 rue Honoré d’Estienne d’Orves ...

    work page doi:10.1016/b978-1-85617-633-0.00001-0 2013