Introduction: José Caballero

Stream: new members

[José Manuel Rodríguez Caballero]

Hello—I'm José Caballero, a PhD candidate at Université Laval working at the intersection of algebraic number theory, high-precision numeric calculations and formal verification. I combine high‑precision PARI/GP computations with Lean proofs to tackle the Stark conjectures and certify properties of Stark units, e.g., the growth of the coefficients of their minimal polynomials. After publishing formal work in Isabelle/HOL, succeeding a course about functional programming in Coq and a course on natural language processing, I'm now exploring AI‑assisted proof generation to accelerate verification. If you’re interested in algebraic number theory and/or AI‑driven formal methods, let’s connect! My Archive of Formal Proofs contributions are listed here (my Estonian email is no longer in use). My website is here.