Related papers: Maintaining a Library of Formal Mathematics
Developing intuition about quantum information theory problems is difficult, as is verifying or ruling-out of hypothesis. We present a Matlab package intended to provide the QIT community with a new and powerful tool-set for quantum…
Models on logarithmic lattices have recently been proposed as an alternative approach to the study of multi-scale nonlinear physics. Here, we introduce LogLatt, an efficient MATLAB library for the calculus between functions on…
The idea of a World digital mathematics library (DML) has been around since the turn of the 21th century. We feel that it is time to make it a reality, starting in a modest way from successful bricks that have already been built, but with…
The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency…
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in…
Large language models (LLMs) have been explored in a variety of reasoning tasks including solving of mathematical problems. Each math dataset typically includes its own specially designed evaluation script, which, while suitable for its…
The ongoing development of Lean 4's Mathlib has produced a macroscopic structural complexity that interweaves logical, mathematical, and infrastructural dependencies. We present a network analysis of this library, extracting its dependency…
This paper presents fairlib, an open-source framework for assessing and improving classification fairness. It provides a systematic framework for quickly reproducing existing baseline models, developing new methods, evaluating models with…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formalize is a Taylor theorem for functions of several variables,…
Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be…
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and…
The prevalence of software systems has become an integral part of modern-day living. Software usage has increased significantly, leading to its growth in both size and complexity. Consequently, software development is becoming a more…
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other…
We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other and providing a flexible interface for extending…
Mean-field games (MFGs) are limiting models to approximate $N$-player games, with a number of applications. Despite the ever-growing numerical literature on computation of MFGs, there is no library that allows researchers and practitioners…
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into…
This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for…
This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language,…
We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting…