Welcome to ANR project FALSE

ANR Project ANR-25-CE40-7639

FALSE is a project bringing together six experts in mathematical formalisation, who work together to formalise in the Lean proof assistant certain key results in algebraic number theory and arithmetic geometry.

The goal of FALSE is to make progress towards formalising the Langlands program, the first step being the definition of the Galois representation attached by Deligne to a modular form. To advance towards this long-term objective, four main themes will be developed by the members of FALSE: class field theory, p-adic modular forms “à la Serre”, the Galois representation associated to an elliptic curve, and the formalism of admissible p-adic representations with the definition of certain period rings that appear in p-adic Hodge theory. Alongside these four topics, the project also proposes two PhD subjects, focused on the formalisation of Tate’s thesis and on p-adic analysis.

The project fits within the broader context of recent advances in mathematical formalisation, which is making remarkable progress and attracting the attention of the international mathematical community. Several teams have recently achieved the formalisation of very deep results, from the Liquid Tensor Experiment proposed by Scholze (to which three FALSE members contributed), to the formalization of the proof of the polynomial Freiman-Ruzsa conjecture by Tao, to the results obtained by the AI AlphaProof, by Google DeepMind, trained in Lean. The advances made by FALSE will open the way to tackle analogously ambitious projects, both in the field of algebraic number theory and of arithmetic geometry.