Riccardo Brasca

collaborators

2 papers

cs.FL2024

A complete formalization of Fermat's Last Theorem for regular primes in Lean

Alex Best, Christopher Birkbeck, Riccardo Brasca +3

We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstr…

math.NT2020

$p$ -adic families of modular forms for Hodge type Shimura varieties with non-empty ordinary locus

Riccardo Brasca

We generalize some of the results of Andreatta, Iovita, and Pilloni and the author to Hodge type Shimura varieties having non-empty ordinary locus. For any $p$ -adic weight $κ$ , we…

A complete formalization of Fermat's Last Theorem for regular primes in Lean

p-adic families of modular forms for Hodge type Shimura varieties with non-empty ordinary locus

$p$ -adic families of modular forms for Hodge type Shimura varieties with non-empty ordinary locus