In this project, I provide a complete, human-readable description for every one of Mathlib4's 9,150 modules — the mathematics library of the Lean 4 proof assistant — stating what each module contains, who uses it, and, wherever the names alone would leave it ambiguous, how it differs from its similarly named neighbors. Coverage is total rather than representative: every directory and every file, described against one fixed, fully specified reference snapshot, released as an independent, open-source resource for the Lean and Mathlib community — not an official product of either. Every entry in this glossary, without exception, is checked against the actual Mathlib4 source at the reference snapshot (Lean 4.29.1, Mathlib4 commit 1ad783f9bf, 2026-05-09): of 9,150 entries, 9,107 carry Complete status and 43 carry Benchmark Theorem status; zero are Pending, and zero are Needs Review. Ismail's Glossary covers the full Mathlib4 hierarchy — 1,129 directories and 8,021 files across six depth levels, spanning all 32 of Mathlib's top-level mathematical domains, from algebra and analysis to category theory and measure theory. Each entry carries six structured fields (path, name, type, parent path, depth, description), so the same data serves a human reader and a retrieval pipeline equally well.The Glossary JSON. The complete dataset, all 9,150 entries, in machine-readable form for any AI platform or retrieval pipeline.The RAG JSON. A flat, embedding-ready export with each entry pre-merged into a single field, for retrieval-augmented-generation systems that want a drop-in data source.The Claude Skill. A self-contained bundle that installs the glossary as an active, queryable reference inside Claude, so Mathlib navigation answers are grounded in current data rather than a language model's frozen training-time memory.The Master Spreadsheet. The live, community-editable source of truth, with a static snapshot published alongside it for anyone who needs a fixed, citable copy.The Interactive Website. A searchable glossary tree plus a dedicated visual Atlas of all 32 top-level domains, built for orientation rather than lookup, alongside a Lean 4 syntax reference and a getting-started guide. To this project's knowledge, no existing Mathlib tool — declaration search engine, in-editor tactic, or auto-generated documentation — provides complete, structural, plain-language coverage of the library at this depth; each presupposes that the user already knows, at least approximately, what they are looking for. All data is provided in full transparency and community contribution is actively encouraged: the complete glossary, every deliverable described above, and the moderated contribution workflow are at github.com/M-Ismail-ZA/IsmailsGlossary. For any feedback, corrections, or collaboration, please contact me via the email address listed on the paper.
Open access
2 source records
Mathematics, Computing, and Information Processing
Nobuki Fujimoto, Rei, (Anthropic, claude-opus-4-7), Claude
⚠v0.0 OUTLINE intentional publication — Pattern 4 mitigation embedded. This is an OUTLINE, not a v0.1 publishable manuscript. The central operational claim — that Rei provides a formal-verification compilation pass composing with AI hypothesis generators (AlphaEvolve, LLM Wiki, OpenEvolve) — requires at least one end-to-end demonstration before v0.1 promotion. As of 2026-05-22 the demonstration is at scaffold-level smoke-run stage only (OpenEvolve scaffold structurally validated, but full 100-iteration evolutionary loop with real evolved Lean 4 proof NOT YET executed). Publication-as-v0.0 is intentional honest framing per OUKC feedback_no_rush_publication.md: rather than wait silently for v0.1 evidence, the OUTLINE is published with explicit gate state so reviewers can see exactly what is and is not claimed. Framing concept: AlphaEvolve / LLM Wiki / OpenEvolve = hypothesis generators (loosely-grounded, fast, large-search). Rei = proof completer (mechanically verified, slow, decisive). Together they compose: hypothesis generator emits candidates → Rei evaluates via D-FUMT₈ 8-axis projection (γ-evaluator) + Lean 4 zero-sorry validation (β-evaluator) → return verified candidates to the evolutionary loop. Rei is positioned as a formal-verification compilation pass in the AI-mathematics generation pipeline. Scaffold evidence (2026-05-22): external/openevolve-rei/ — YAML config (Ollama 3-prover ensemble), Python evaluators (β = Lean 4 zero-sorry, γ = D-FUMT₈ projection), example skeleton (26-circle packing 2.635 benchmark). 4 smoke-tests PASS: yaml parse + 3 Python AST parse + circle_packing standalone execution (n=26 r=0.4167 density=14.18) + γ-evaluator returns OpenEvolve-compatible dict with metrics (axis_dominant=ZERO 9 hits, score=0.0154) + artifacts (token_count=13). Per SCOPE.md non-claims: this is NOT a fork of OpenEvolve, NOT a claim of 26-circle 2.635 reproduction, NOT a claim that Rei has built an evolutionary code generator, NOT a paper-publishable result by itself. v0.1 acceptance criteria (10 items): see §9. Core gates: OpenEvolve installed + first 100-iteration loop completes + real evolved Lean 4 proof generated + scaffold extended with at least one zero-sorry proof for one open conjecture from META-DB Tier 1. v0.1 will publish as Zenodo new-version preserving DOI lineage from this v0.0 record. Honest scope (read first): (1) This is OUTLINE only — framing + prior-art audit + acceptance criteria, no end-to-end evidence. (2) Rei is NOT a hypothesis generator — its role in this composition is specifically as the verifier/completer. (3) Per feedback_world_uniqueness_claim_controllable.md: we use "to our knowledge no equivalent Lean 4 zero-sorry + D-FUMT₈ 8-axis evaluator exists in the OpenEvolve plugin ecosystem as of 2026-05-22" phrasing, NOT "world-first." (4) Three-party co-authorship (Fujimoto / Rei / Claude) per OUKC charter v1.0. (5) Per OUKC No-Patent Pledge — no patent will be filed.
Open access
2 source records
Mathematics, Computing, and Information Processing
While Large Language Models have achieved notable success on formal mathematics benchmarks such as MiniF2F, it remains unclear whether these results stem from genuine logical reasoning or semantic pattern matching against pre-training data. This paper identifies Architectural Reasoning: the ability to synthesize formal proofs using exclusively local axioms and definitions within an alien math domain, as the necessary ability for future automated theorem discovery AI. We use the Obfuscated Natural Number Game, a benchmark to evaluate Architectural Reasoning. By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment. We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time. The results also reveal a divergence in robustness: while general models (Claude-Sonnet-4.5, GPT-4o) suffer performance degradation, reasoning models (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) maintain the same accuracy despite the absence of semantic cues. These findings provide a quantitative metric for assessing the true capacity for mathematical reasoning.
Open access
3 source records
Mathematics, Computing, and Information Processing
Pierpaolo Della Monica, Ivan Visconti, Andrea Vitaletti, Marco Zecchini
An essential requirement for the large-scale adoption of Web3 is enabling users to benefit from their data even within already deployed systems. This raises an important open question: how can existing, widely adopted software verify that a user has retrieved specific data from a TLS server? Impressive scientific results (e.g., DECO [CCS20] and the work of Xie et al. [USENIX24]) and industrial products (TLSNotary) have recently made progress in the above challenging direction. However, while they nicely leave TLS servers untouched, the retrieved data is then used in computations with verifiers that are required to run some advanced non-standardized cryptographic schemes (e.g., ZK-SNARKs), which clearly limits the large-scale adoption of the proposed technologies. In this paper, building on top of previous approaches and relying on the recent concept of Predicate Blind Signatures of Fuchsbauer and Wolf [Eurocrypt24], we bypass the limits of prior work by presenting ACTS a distributed architecture that, while still leaving TLS servers untouched, it allows a user to show possession of data retrieved from TLS servers simply requiring that the software of the verifier can check a standard signature. Our contributions include a round-optimal predicate blind signature protocol that produces standard RSA-PSS signatures. We show how this primitive can be integrated into the DECO architecture (and its successors) to certify data retrieved from TLS servers. Furthermore, we have optimized our construction to make it practical on commodity hardware for a large and significant class of policies implemented by the notary (i.e., the actor that is in charge of obliviously certifying TLS data, therefore preserving data confidentiality). We provide an experimental evaluation on the simple but powerful enough use case of a PDF document downloaded from a TLS server and encoded into an AES-GCM ciphertext. The user will then get a certified PDF through a standard PADES signature added obliviously to the PDF along with some metadata by a notary service. The resulting standard signed PDF document can be transparently verified using off-the-shelf PDF readers. Our experimental validation demonstrates that our architecture is suitable for real-world deployment in concrete scenarios.
Zero-knowledge proofs (ZKPs) are increasingly deployed in domains such as privacy-preserving authentication, verifiable computation, and secure finance. However, authoring ZK programs remains challenging: unlike conventional software development, ZK programming manifests a fundamental paradigm shift from \textit{imperative computation} to \textit{declarative verification}. This process requires rigorous reasoning about finite field arithmetic and complex constraint systems (which is rare in common imperative languages), making it knowledge-intensive and error-prone. While large language models (LLMs) have demonstrated strong code generation capabilities in general-purpose languages, their effectiveness for ZK programming, where correctness hinges on both language mastery and constraint-level reasoning, remains unexplored. To address this gap, we propose \textsc{ZK-Eval}, a domain-specific evaluation pipeline that probes LLM capabilities on ZK programming at three levels: language knowledge, algebraic primitive competence, and end-to-end program generation. Our evaluation of four state-of-the-art LLMs reveals that while models demonstrate strong proficiency in language syntax, they struggle when implementing and composing algebraic primitives to specify correct constraint systems, frequently producing incorrect programs. Based on these insights, we introduce \textsc{ZK-Coder}, an agentic framework that augments LLMs with constraint sketching, guided retrieval, and interactive repair. Experiments with GPT-o3 on Circom and Noir show substantial gains, with success rates improving from 20.29\% to 87.85\% and from 28.38\% to 97.79\%, respectively. With \textsc{ZK-Eval} and \textsc{ZK-Coder}, we establish a new basis for systematically measuring and augmenting LLMs in ZK code generation to lower barriers for practitioners and advance privacy computing.
Open access
2 source records
Mathematics, Computing, and Information Processing
Katharina Koschatko, Reinhard Lüftenegger, Christian Rechberger
Gröbner basis cryptanalysis of hash functions and ciphers, and their underlying permutations, has seen renewed interest recently. Anemoi (Crypto’23) is a permutation-based hash function that is efficient for a variety of arithmetizations used in zero-knowledge proofs. In this paper, exploring both theoretical bounds as well as experimental validation, we present new complexity estimates for Gröbner basis attacks on the Anemoi permutation over prime fields.We cast our findings in what we call the six worlds of Gröbner basis cryptanalysis. As an example, keeping the same security arguments of the design, we conclude that at least 41 instead of 37 rounds would need to be used for 256-bit security, whereby our suggestion does not yet include a security margin.
Open access
Polynomial and algebraic computation
Cryptography and Residue Arithmetic
Mathematics, Computing, and Information Processing
Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olšák · 6 authors
The development of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is therefore to make use of SAT solvers in expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is synthesizing the appropriate instances from the typically infinite Herbrand universe. In this work, we develop a machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on a graph neural network (GNN) that learns from problems and their solutions independently of many symmetries and symbol names (addressing the abundance of Skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then combined with an efficient ground solver and, starting with zero knowledge, iteratively trained on a large corpus of mathematical problems. We show that the system is capable of solving many problems by such educated guessing, finding proofs for 32.12% of the training set. The final trained system solves 19.74% of the unseen test data on its own. We also observe that the trained system finds solutions that the iProver and CVC5 systems did not find.
Open access
Natural Language Processing Techniques
Handwritten Text Recognition Techniques
Mathematics, Computing, and Information Processing
The secondary market for Ethereum non-fungible tokens (NFTs) has resulted in over $1.8bn being paid to creators in the form of a sales tax commonly called creator royalties. This was despite royalty payments being enforced by no more than social contract alone. Predictably, such an incentive structure led to zero-royalty alternatives becoming abundant and payments dwindled. A purely programmatic solution to royalty enforcement is hampered by the prevailing NFT standard, ERC-721, which is ignorant of sale values and royalty enforcement therefore relies on (potentially dishonest) third parties. We thus introduce an incentive-compatible mechanism for which there is a single rationalisable solution, in which royalties are paid in full, while maintaining full ERC-721 compatibility. The mechanism constitutes the core of ERC-7526.
The cipher (or athbash, under which name Web3 defines it) is a Hebrew substitution cipher which replaces the first letter of the Hebrew alphabet (aleph, 1\) by the last (tav, ) the second (beth, J) by the last but one (shin, IJI), and so on, unti I we get to the last (ta , n), which i replaced by the first (aleph, 1\). Jan Anderson described it in Fledge Ledge Edge (WW 8. 1997229). Naturally, the idea can be applied to our alphabet; following the precedent set by atbash I name it the azby cipher.