arXiv subjects

Alain Chavarri Villarello

Publications and source records attributed to Alain Chavarri Villarello.

4 recordsLinked to original sources

arXiv2026

Leiden Declaration on Artificial Intelligence and Mathematics

This declaration calls for action to address the challenges posed by the use of artificial intelligence within mathematics research. Technological developments have repeatedly transformed the practice of mathematics. Recent artificial intelligence technologies, including symbolic and neural methods for the generation and formalization of mathematics, may already have initiated a significant chapter in this long history. Among researchers, artificial intelligence has produced a wide range of reactions: enthusiasm for its potential to yield new discoveries; intimidation by the pace of developments; indifference to these rapid changes; and concern for the implications, both for mathematics and in wider society. Mathematicians have a choice about whether and how to adopt artificial intelligence in the conduct of their research. They also have a responsibility to ensure the continued flourishing of the discipline. This Declaration calls upon mathematicians to exercise this responsibility, and provides recommendations for individuals, institutions, government, and industry. Although we adopt the perspective of mathematical research, much of what we write applies equally to other aspects of mathematics. This includes work in the broader mathematical sciences, education, mentoring, publishing, funding, science policy, and use of mathematics in the wider world.

math.HO↗

arXiv2026

Formally certifying number field invariants

Number fields, which generalize the rational numbers, are fundamental objects in number theory. Many of their key arithmetic properties are captured by invariants whose computation is among the central tasks of computational algebraic number theory and a focus of several computer algebra systems and databases. In this paper, we describe a Lean 4 formalization for certifying several of these number field invariants. Building on previous work on certifying rings of integers, we extend this certification approach to further invariants including the signature, the unit group modulo $p$-th powers, and, ultimately, the class group. We also improve discriminant certification, allowing verifications for higher-degree number fields infeasible in previous work. We introduce structures based on representations of algebraic objects suited to computation, including reusable ones for certifying ideal arithmetic. Along the way, we formalize several underlying mathematical results, for instance on real closed fields and pseudo-remainder sequences, which are of independent interest. We apply our framework to verify hundreds of entries of the $\textit{L-functions and modular forms database}$ (LMFDB) concerning the discriminant, signature, class number, and class group structure of various number fields. To this end, we wrote a SageMath script that computes the certificates and outputs Lean proofs of the corresponding statements.

cs.LO↗

arXiv2025

Certifying rings of integers in number fields

Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the $\textit{Number fields}$ section of the $\textit{L-functions and modular forms database}$ (LMFDB). These concern, for several number fields, the explicitly given $\textit{integral basis}$ of the ring of integers and the $\textit{discriminant}$. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.

cs.LO↗

arXiv2020

Representing partition lattices through FCA

We investigate the standard context, denoted by $\mathbb{K}\left(\mathcal{L}_{n}\right)$, of the lattice $\mathcal{L}_{n}$ of partitions of a positive integer $n$ under the dominance order. Motivated by the discrete dynamical model to study integer partitions by Latapy and Duong Phan and by the characterization of the supremum and (infimum) irreducible partitions of $n$ by Brylawski, we show how to construct the join-irreducible elements of $\mathcal{L}_{n+1}$ from $\mathcal{L}_{n}$. We employ this construction to count the number of join-irreducible elements of $\mathcal{L}_{n}$, and show that the number of objects (and attributes) of $\mathbb{K}\left(\mathcal{L}_{n}\right)$ has order $Θ(n^2)$.

math.CO↗