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
In todayâs digital age, the verification of documents is a critical aspect of numerous transactions and processes across various industries. However, traditional methods of document verification are often susceptible to fraud, tampering, and inefficiencies. In response to these challenges, this project proposes a novel solution leveraging blockchain technology to enhance the security and integrity of document verification processes. The objective of this project is to develop a decentralized system for document verification using blockchain, aiming to provide a secure, transparent, and tamper-proof platform for verifying the authenticity of digital documents. By harnessing the immutable and transparent nature of blockchain, the proposed system seeks to address the shortcomings of traditional verification methods and establish a trusted environment for document verification. Key features of the proposed system include the use of cryptographic hashing techniques to create unique digital fingerprints for each document, which are then stored on a blockchain network. Smart contracts are utilized to automate the verification process, enabling seamless and transparent verification without the need for intermediaries.The methodology involves the design and implementation of the blockchain-based document verification platform, incorporating essential components such as user authentication, document uploading, verification, and retrieval functionalities. The system is developed using Ethereum, a popular blockchain platform, and is deployed on a test network for evaluation and testing. Results from experimental testing demonstrate the effectiveness and reliability of the proposed system in providing tamper-proof document verification services. Furthermore, comparative analysis with existing centralized solutions highlights the advantages of blockchain-based verification in terms of security, transparency, and efficiency.
2 source records
Web Data Mining and Analysis
Semantic Web and Ontologies
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.
Know Your Customer (KYC) is a costly and heavily regulated process that financial institutions are legally required to undertake to conduct business with their customers. Distributed Ledger Technology (DLT) can be used as a coordination mechanism for financial institutions to share KYC costs in a common jurisdiction. Previous techniques that use DLT to support the KYC process, perhaps unexpectedly, introduce a single point of failure in the system. Indeed, financial institutions are vulnerable to repercussions if a single institution makes an operational mistake during the onboarding stage. We tackle this problem by introducing a probabilistic mechanism, where some of the financial institutions involved need to independently repeat the KYC process in the form of a randomised audit. This novel approach mitigates the single point of failure of the previous DLT-based KYC designs and introduces a natural trade-off between the security of the KYC process and its cost efficiency. In our approach the audit probability can be either set as a global DLT parameter or be dependent on attributes associated with the particular client.
Mathematics, Computing, and Information Processing
Looping of the colonoscope shaft is the most common problem associated with a colonoscopy procedure. One study has shown that looping occurred in 91 out of 100 cases [1]. Looping can have a variety of effects ranging from extended procedure times, incomplete examinations, or even perforation of the colon wall [2]. Another study shows that 37 perforations occurred in 116,000 patients [3]. Looping increases discomfort for the patient, requiring larger amounts of anesthesia, and increasing operation time. Looping forces the doctor to reposition the colonoscope by twisting and retracting the shaft with varying degrees of success. This additional maneuvering of the colonoscope shaft during the procedure places extra stress on the inner lining of the colon wall.The problem of looping can be lessened with the help of manipulation by the doctor. By applying pressure to the abdomen and rotating the patient on his/her left or right side, looping can be reduced [4]. Some examples of existing equipment that is currently used to help combat this problem include: a double balloon sheath around the distal tip, a shape locking overtube guide, a general overtube, or a variable stiffness colonoscope. These are devices that passively prevent looping from forming. A better way to try and solve this problem is to constantly monitor the shape of the colonoscope shaft to determine if and when a loop will form and prevent it from happening. Some of the devices that employ a similar method to this include: the computer assisted NeoGuide system, fluoroscopy, and magnetic endoscopic imaging. The first of these devices uses a computer controlled, articulated colonoscope such that each segment follows the exact same path as the segment preceding it. The latter two give the doctor a 3D image of the shaft. If these devices were less expensive, then they might be more widely used, but as it is they are very expensive.With this in mind, a proof of concept method for detecting the shape of the colonoscope shaft during the procedure is introduced. If the shape of the colonoscope shaft is known then looping can be detected and avoided more easily. It would be more beneficial to avoid a loop all together than to backtrack once it is already formed.A model was developed that consists of multiple sets of connected links to be placed along the middle of the colonoscope shaft. These links are free to rotate in two different directions to show the motion of the shaft in full. Each rotation joint is equipped with a 6 mm rotational potentiometer, an angular displacement sensor. The potentiometer is a variable resistor that increases its resistance linearly from zero to a peak value over a range of 240 deg. Every rotation joint has a potentiometer attached to it through a modified pin. Figure 1 shows a single link with potentiometer attached.This only shows a single link but the entire model has 20 links connected together to give an image of a much larger stretch of the colonoscope. The link system is designed to conform to the inside of the colonoscope shaft only increasing the stiffness marginally. The system setup is shown in Fig. 2.Figure 2 above shows the complete system diagram with all components and order of attachment. Once the model was finished it each sensor was wired together in series on the power and ground pins with a power supply. The sensor output pins were wired separately and returned to the end of the system to a data acquisition device to process the signals. The signals acquired are voltage readings from each potentiometer. Signal express was used to acquire the signal and save it as a file. The file was then inserted into a computer program in matlab, which graphed an image of the model.The linkage was formed into a straight line to show the baseline reading for the system. The second configuration was a small alpha loop with 3 cm radius. This was formed because the alpha loop is one of the most common types of loops found in the colonoscopy procedure. Both configurations are shown in Fig. 3.Once this was done, the voltage readings from the sensors were recorded into a file. This file was then inserted into a program that manipulates these values into corresponding angles based upon calibration charts. From the corresponding angles a graphical image was produced that closely resembles the original model. The matlab graphs are set to the same scale as the original model. The graphical images can be seen in Fig. 4. The straight line and alpha loop configuration both very accurately resemble the physical model with little error (Figs. 4(a) and 4(b)). This shows that the model can accurately predict complex shapes and configurations, with little error, that are commonly found inside the colon during a procedure.From the results presented above, it can be seen that the linkage model method with attached potentiometers can easily manage loops commonly found in the everyday procedure. This ability combined with the graphical imaging software can help a doctor to potentially see a loop as it is about to be formed. As has been previously said, the key to stopping loop formation is the prediction of loops before they form. With this model and software, loops can be accurately predicted and viewed during a procedure. With little to no training at all a doctor can look at the computer screen and be able to tell if the shaft of the colonoscope is approaching the tipping point between loop formation and following the colon wall around a curve such as in the sigmoid colon. This would be greatly helpful with decreasing the numbers of incomplete colonoscopies due to loop formation. Along with this, knowing the curvature of the shaft of the colonoscope and the basic knowledge of the shape of the colon, the doctor can give a more accurate description of locations of polyps discovered in the colon.Overall, this method of loop detection that has been discussed could serve as an additional tool to helping a doctor complete a colonoscopy procedure. This method could reduce procedure time due to loop formation as well as decrease pain to the patient. The doctor could also decrease the number of incomplete colonoscopies that result from looping of the colonoscope shaft.
Soft Robotics and Applications
Mathematics, Computing, and Information Processing
Yi Deng, Juan A. Garay, San Ling, Huaxiong Wang · 5 authors
Abstract. In 2001, a breakthrough result by Barak [FOCS 2001] showed how to achieve public-coin zero-knowledge (ZK) arguments in constant rounds, a feature known to be impossible using black-box simulation. In this approach, the simulator makes use of the code of the malicious verifier in computing the prover messages (albeit without understanding it), and does not rewind the malicious verifierâand it is hence called a straight-line simulator. Since then, however, we have witnessed little progress on the basic question whether Barakâs technique can be extended to ZK proof systems. In this paper we make progress on this front, by providing strong evidence that such an extension is far from likely. Specifically, we show that for a natural class of constant-round public-coin ZK proofs (which we call âcanonical, â as all known non-black-box ZK protocols fall in this category), a straight-line simulator based on the known non-black-box technique for such a proof system can actually be used to solve a seemingly unrelated problem, namely, to figure out some non-trivial property of a verifierâs program, and without executing the target code, a problem commonly viewed as notoriously hard. A key tool in our reduction is an improved structure-preserving version of the well-known Babai-Moran Speedup (derandomization) Theorem, which essentially says that, for a constant-round public-coin interactive proof system in which the verifier sends m messages and each of the prover messages is of length p, if the cheating probability for an unbounded prover is Ï”, then there exist (p/O(log 1
Mathematics, Computing, and Information Processing
Claus Huitfeldt, Yves Marcoux, C. M. Sperberg-McQueen
The type/token distinction introduced by C. S. Peirce and taken up by many others is familiar when applied to individual symbols or characters in a writing system, and also when applied at a higher level to words (and word-like objects). Some writers apply the distinction not only at some basic or foundational level but also as a description of higher levels of organization. This paper follows their example by outlining a concrete extension of the type/token distinction to all levels of document organization, specifying that higher-level types may contain sequences of lower-level types, and similarly for higher- and lower-level tokens. We further extend the usual model of types and tokens by allowing higher-level types to contain not just sequences of (lower-level) types but also sets, bags, conjunctions and disjunctions of types. This allows the system to deal gracefully both with indeterminate documents (e.g., a manuscript in which it is not clear whether a given mark on the page represents a 'c' or a 't') and with intentionally polyvalent documents, in which some marks are to be read as tokens of more than one type, as in the âambigramâ, a sort of combination puzzle and calligraphic artwork in which the shapes on the page may be read in different ways, or the same way, in different directions. This account of document structure in terms of types and tokens is similar in many ways to that offered by SGML, XML, and other systems of descriptive markup. On this view, SGML and XML elements are, strictly speaking, types (and tokens) in Peirce's sense of those words. Some techniques developed in other areas to which the type/token distinction is relevant may be useful in work on markup languages (and vice versa).
Digital Humanities and Scholarship
Mathematics, Computing, and Information Processing
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.