arXiv subjects

Micaela Mayero

Publications and source records attributed to Micaela Mayero.

13 recordsLinked to original sources

arXiv2026

A Rocq Formalization of Simplicial Lagrange Finite Elements

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.

cs.LO↗

arXiv2025

A Rocq Formalization of Monomial and Graded Orders

Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article is therefore definitions, operators, and proofs of properties about relations and orders, thus providing a comprehensive Rocq library. We especially focus on monomial orders, that are total orders compatible with the monoid operation. More than its definition and proved properties, we define several of them, among them the lexicographic and grevlex orders. For the sake of genericity, we formalize the grading of an order, a high-level operator that transforms a binary relation into another one, and we prove that grading an order preserves many of its properties, such as the monomial order property. This leads us to the definition and properties of four different graded orders, with very factorized proofs. We therefore provide a comprehensive and user-friendly library in Rocq about orders, including monomial and graded orders, that contains more than 700 lemmas.

cs.LO↗

arXiv2025

Maths with Coq in L1, a pedagogical experiment

In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years. These students are in a double major mathematics and computer science curriculum. The course is mandatory and consists only of hands-on sessions with the Coq proof assistant. We present some of the practical sessions worksheets, the methodology we used to write them and some of the pitfalls we encountered. Finally we discuss how this course evolved over the years and will see that there is room for improvement in many different technical and pedagogical aspects.

cs.LO↗

arXiv2024

Teaching Divisibility and Binomials with Coq

The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.

cs.LO↗

arXiv2022

Lebesgue Induction and Tonelli's Theorem in Coq

Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $σ$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.

cs.LO↗

arXiv2021

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $σ$-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou's lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of $L^p$~spaces such as Banach spaces.

cs.LO↗

arXiv2012

Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.

math.NA↗

arXiv2011

Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.

cs.LO↗

arXiv2010

Formal Proof of a Wave Equation Resolution Scheme: the Method Error

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.

cs.LO↗

arXiv2010

Formal Proof of SCHUR Conjugate Function

The main goal of our work is to formally prove the correctness of the key commands of the SCHUR software, an interactive program for calculating with characters of Lie groups and symmetric functions. The core of the computations relies on enumeration and manipulation of combinatorial structures. As a first "proof of concept", we present a formal proof of the conjugate function, written in C. This function computes the conjugate of an integer partition. To formally prove this program, we use the Frama-C software. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program.

cs.LO↗

arXiv2010

Formal Proof of a Wave Equation Resolution Scheme: the Method Error

cs.LO↗

arXiv2006

The Three Gap Theorem (Steinhauss Conjecture)

We deal with the distribution of N points placed consecutively around the circle by a fixed angle of a. From the proof of Tony van Ravenstein, we propose a detailed proof of the Steinhaus conjecture whose result is the following: the N points partition the circle into gaps of at most three different lengths. We study the mathematical notions required for the proof of this theorem revealed during a formal proof carried out in Coq.

cs.LO↗

arXiv2005

Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant

We present the proof of Diophantus' 20th problem (book VI of Diophantus' Arithmetica), which consists in wondering if there exist right triangles whose sides may be measured as integers and whose surface may be a square. This problem was negatively solved by Fermat in the 17th century, who used the "wonderful" method (ipse dixit Fermat) of infinite descent. This method, which is, historically, the first use of induction, consists in producing smaller and smaller non-negative integer solutions assuming that one exists; this naturally leads to a reductio ad absurdum reasoning because we are bounded by zero. We describe the formalization of this proof which has been carried out in the Coq proof assistant. Moreover, as a direct and no less historical application, we also provide the proof (by Fermat) of Fermat's last theorem for n=4, as well as the corresponding formalization made in Coq.

cs.LO↗