1 Introduction

This blueprint covers the classical part of the Lean 4 library diaz-modulus-lean: the theorems of transcendental number theory in the table “The classical theorems” of its README, and every result their proofs use. They are the theorems of Hermite–Lindemann and Lindemann–Weierstrass, the Gelfond–Schneider theorem and the transcendence of \(e^{\pi }\), the six exponentials theorem, the four exponentials theorem in transcendence degree one, Waldschmidt’s theorem of 1973 with Schneider’s eighth problem, Roy’s lemma on singular spaces of matrices, and Baker’s theorem, by the criterion of Schneider–Lang in several variables; on the way, Waldschmidt’s transcendence criterion and his zero count for exponential polynomials. These chapters claim no new transcendence theorem. Later chapters, added in October 2026, hold results of the library’s work on Diaz’s conjecture that were not found in the sources read: what rank-one configurations can see near a point of a circle (Chapter 10), a dichotomy for \(\mathrm{Li}_2(1/2)\) (Chapter 11), quadratic relations near a point of a circle (Chapter 12), and consequences in transcendence degree one (Chapter 13). Chapter 14 lists these results and says which of them are not routine; in the dependency graph those have a double border. The library’s other results on Diaz’s conjecture, the case analysis that reduces it to two open statements, are not part of this blueprint.

Every result here is a separate statement with its own Lean proof, and every one is proved: the library depends only on Lean’s three standard axioms. Each is a node proved on the platform Prove2Me (https://prove2.me) and ported to the library, and the dependencies shown are the imports of the accepted proofs, with one exception noted at Theorem 3.3. Each statement names its Lean declaration and was checked against it; where a Prove2Me page states a result in another form, the statement here follows the Lean declaration. An algebraic number is a complex number algebraic over \(\mathbb {Q}\), a logarithm of an algebraic number is a complex number \(\ell \) with \(e^{\ell }\) algebraic, and \(\mathbb {N}\) contains \(0\).

Three parts come from elsewhere. The Lindemann–Weierstrass development is ported from Mathlib pull request #28013 by Yuyang Zhao, which is not merged. The proof of the Gelfond–Schneider theorem restructures the formalisation of M. Karatarakis and F. Wiedijk [ KW26 ] . The statement e_pi_transcendence is a node posed on Prove2Me by another contributor; the proof here applies Gelfond–Schneider.

Almost all of this library was written by AI agents, working on the Prove2Me platform under the direction of Carlo Perassi: Anthropic’s Claude, run through Claude Code. The agents wrote the Lean statements and proofs, the texts of the platform pages, most of the library’s companion note, the literature checks, and this blueprint. Carlo chose the problem and the direction, set the rules the agents work under, and approved every publication; Carlo read the statements and the companion note, not the Lean proofs line by line. Lean checks that every proof proves its statement. It does not check that a statement says what the cited source says: the agents compared each statement and attribution with the primary sources, often from page images.