6 citations · 10 across the 5 of their papers we have counts for
6 papers
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for ch…
Certifying rings of integers in number fields
Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen
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 sys…
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola +1
Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form , where is a (gi…
Use and abuse of instance parameters in the Lean mathematical library
Anne Baanen
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Rela…
A formalization of Dedekind domains and class groups of global fields
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan +1
Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental pro…
Combining predicate transformer semantics for effects: a case study in parsing regular languages
Anne Baanen, Wouter Swierstra
This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our p…