40.2k citations · 63.8k across the 6 of their papers we have counts for
7 papers
Advancing Mathematics Research with AI-Driven Formal Proof Search
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to gener…
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
Moritz Firsching, Paul Lezeau, Salvatore Mercuri +8
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this,…
Multiple-inheritance hazards in dependently-typed algebraic hierarchies
Eric Wieser
Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arrang…
Formalizing Geometric Algebra in Lean
Eric Wieser, Utensil Song
This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, ma…
Scalar actions in Lean's mathlib
Eric Wieser
Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses a…
Array Programming with NumPy
Charles R. Harris, K. Jarrod Millman, Stéfan J. van der Walt +23
Array programming provides a powerful, compact, expressive syntax for accessing, manipulating, and operating on data in vectors, matrices, and higher-dimensional arrays. NumPy is t…