Automatic Theorem Proving

• Visa Nummelin, Jasmin Blanchette, and Sander R. Dahmen, Recurrence-Driven Summations in Automated Deduction, Proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023), Springer series Lecture Notes in Artificial Intelligence, 23--40; also see the technical report.

Number Theory/Arithmetic Geometry (incl. Formal Theorem Proving)

• with Anne Baanen and Alain Chavarri Villarello, Certifying rings of integers in number fields, Preprint, 14 pp., accepted for publication in CPP 2025.
• with Joey M. van Langen, Explicitly bounding perfect powers in elliptic divisibility sequences, Preprint, 23 pp.
• with Anne Baanen, Alex J. Best, and Nirvana Coppola, Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), 47--62.
• with Anne Baanen, Ashvni Narayanan, and Filippo A. E. Nuccio, A formalization of Dedekind domains and class groups of global fields, Journal of Automated Reasoning. 66 (2022), no. 4, 611--637.
• with Anne Baanen, Ashvni Narayanan, and Filippo A. E. Nuccio, A formalization of Dedekind domains and class groups of global fields, pages 12:1–-12:19 of Liron Cohen and Cezary Kaliszyk (editors), 12th International Conference on Interactive Theorem Proving (ITP 2021), LIPIcs vol. 193, 2021.
• with Johannes Hölzl and Robert Y. Lewis, Fomalizing the solution to the cap set problem, pages 15:1--15:19 of John Harrison, John O’Leary, and Andrew Tolmach (editors), 10th International Conference on Interactive Theorem Proving (ITP 2019), LIPIcs vol. 141, 2019.
• with Arno Kret, Andrew Wiles and the Abel Prize (in Dutch), Nieuw Arch. Wiskd. (5) 18 (2017), no. 2, 88--98.
• with Michael A. Bennett, Maurice Mignotte, and Samir Siksek, Shifted powers in binary recurrence sequences, Math. Proc. Camb. Phil. Soc. 158 (2015), no. 2, 305--329.
• with Michael A. Bennett, Imin Chen, and Soroosh Yazdani, Generalized Fermat equations: a miscellany, Int. J. Number Theory. 11 (2015), no. 1, 1--28.
• with Samir Siksek, Perfect powers expressible as sums of two fifth or seventh powers, Acta Arith. 164 (2014), no. 1, 65--100.
• with Michael A. Bennett, Imin Chen, and Soroosh Yazdani, On the equation a³+b³ⁿ=c², Acta Arith. 163 (2014), no. 4, 327--343.
• with Michael A. Bennett, Klein forms and the generalized superelliptic equation, Ann. of Math. 177 (2013), no. 1, 171--239.
• with Soroosh Yazdani, Level lowering modulo prime powers and twisted Fermat equations, Canad. J. Math. 64 (2012), no. 2, 282--300.
• A refined modular approach to the Diophantine equation x²+y²ⁿ=z³, Int. J. Number Theory 7 (2011), no. 5, 1303--1316.
• with Michael Coons, On the residue class distribution of the number of prime divisors of an integer, Nagoya Math. J. 202 (2011), 15--22.
• with Nils Bruin, Visualizing elements of Sha[3] in genus 2 jacobians, pages 110--125 of Guillaume Hanrot, François Morain, and Emmanuel Thomé (editors), Algorithmic Number Theory, 9th International Symposium, LNCS 6197, Springer--Verlag, 2010.
• Classical and modular methods applied to Diophantine equations, Ph.D. Thesis (2008), Utrecht University, ISBN: 978-90-393-4867-3.
• Lower bounds for numbers of ABC-hits, J. Number Theory 128 (2008), no. 6, 1864--1873.
• Counting integral Lamé equations by means of dessins d'enfants, Trans. Amer. Math. Soc. 359 (2007), no. 2, 909--922.

Other

• with van den Berg et al., Understanding the electromagnetic field in an MRI scanner, Proceedings of the 58th European Study Group Mathematics with Industry (2007), 69--90.

Back to main page