🏛️ ATLAS (Library Blueprints) 🧭 Tour❓ How to use
3papers
76numbered results
26with Lean, whole or a part
43checked by a program
25written proof only

Characters at torsion elements

Published on Zenodo
🏷️ Representation theory · characters of Lie groups 05E10 20G05 17B22 05A15

Characters of Sp(2m) at the powers of Kostant's element

The irreducible characters of Sp(2m) at every power of Kostant's element: when they vanish, their value as a signed ratio of root products, and their absolute value as a product of dimensions of GL, Sp and odd SO representations.

0 / 12 in Lean, whole or a part
10 / 12 checked by a program
2 / 12 written proof only

A result can carry several marks. Each tile opens its statement; the large ones are the main results.

Zeros of weighted character sums

Published on Zenodo
🏷️ Number theory · arithmetic functions 11A25 11K65 11L40 11P70 11R29

Exact zeros of weighted sums of completely multiplicative functions

Zeros of the weighted sums Σn≤m nε(n) of completely multiplicative ε with values ±1: every admissible length is a zero of some ε, infinitely many zeros are rare in measure and generic in category, and for quadratic characters the zeros are explicit.

8 / 17 in Lean, whole or a part
11 / 17 checked by a program
2 / 17 written proof only

A result can carry several marks. Each tile opens its statement; the large ones are the main results.

Rational closure of the free field

v1 (Zenodo)
🏷️ Associative rings · division rings 16K40 16S85 16S10 16S34 16E60

Inversion height two in the free field of the free group: strict hierarchies and a non-membership criterion

Inside the second inversion stage of the free field of the free group of rank three, two chains of subrings are strict at every step and infinitely many stopping steps of the Dubrovin–Gräter–Hanke series occur; the tool is a sufficient criterion for non-membership.

18 / 47 in Lean, whole or a part
22 / 47 checked by a program
21 / 47 written proof only

A result can carry several marks. Each tile opens its statement; the large ones are the main results.

How to read a blueprint

Each numbered result of a paper is one tile and one node of its map, copied verbatim with the paper's numbering. Its colour says what checked it besides the written proof; the map says which results its proof uses.
✅ formalized in Lean
◐ a part in Lean
💻 checked by a program
written proof only

One version, one site

Each site follows the version named on its card and carries that PDF; its Lean links point to a fixed commit.