Blockchain Papers

Jincheng Zhang

This paper presents a novel zero-knowledge proof scheme constructed upon polynomial multi-variable rings. The core claim is to design a scheme that significantly enhances proof efficiency and security while addressing the computational complexity bottlenecks prevalent in existing approaches. The proposed mechanism leverages the unique properties of multi-variable polynomial rings to establish a streamlined proof and verification process, minimizing the risk of information leakage. Unlike traditional zero-knowledge proofs that often rely heavily on large number arithmetic, this scheme utilizes polynomial operations, leading to potentially improved performance. This work contributes to the field of cryptographic primitives by offering a new design paradigm rooted in algebraic structures, potentially unlocking avenues for more efficient and practical zero-knowledge proofs. The key contributions are a novel construction and a theoretical analysis demonstrating the security and efficiency gains. The scheme operates by encoding the statement to be proven as a polynomial equation in a multi-variable ring, and the prover generates a proof that allows the verifier to confirm the equation's validity without learning any information beyond the proof itself. This design aims to provide a more scalable and practical solution for zero-knowledge proof applications.

Akira Toyohara, Ye Tao, Siqiong Yao

No quasiperfect number ($σ(n) = 2n + 1$) is known, and its number of distinct prime factors is bounded below; the bound $ω\ge 7$ of Hagis--Cohen has stood since 1982, obstructed by a family of ``deep leaves'' on which pure enumeration cannot terminate (the scan bound for the intermediate prime reaches $8 \times 10^8$, and the exponent dimension is unbounded). This paper clears that obstruction with three lemmas at the level of secondary-school algebra --- a discriminant criterion, a quadratic-residue sieve, and a multilinear resolver --- which eliminate the last prime $q$, the intermediate prime $p$, and the exponent dimension respectively, turning a non-terminating search into a finite decision. On this basis all 381 stems of ``$3 \mid n$ and $ω= 7$'' and their $79{,}751{,}212$ deep leaves are eliminated, with the ledger closing exactly and zero solutions throughout; the complementary case ``$3 \nmid n$ and $ω= 7$'' collapses to a single stem, which is eliminated directly, so that the proof does not rest on any theorem whose published record we could not independently re-verify. Together with the machine elimination of $ω\le 6$ (Theorem B4), this yields the main theorem: \emph{any quasiperfect number, if one exists, satisfies $ω(n) \ge 8$} --- the first advance of this bound since Hagis--Cohen 1982. The full computation has been reproduced by seven separately closed ledgers across three algorithmic architectures (CPU and GPU), all with zero solutions and exact ledger closure, and the lemma layer is formalized in Lean (259 theorems, zero \texttt{sorry}). A 2023 preprint of Zemann reported the same bound by a different computation; our audit of its public code found a coverage gap of 35 feasible exponents, so the elimination given here is, to our knowledge, the first complete proof. Code, ledgers, and Lean sources are available from the authors.

Shi-Mei Ma

A famous result in the theory of combinatorial polynomials is the real-rootedness of the type $D$ Eulerian polynomial $D_n(x)$, which was originally conjectured by Brenti in 1994. By constructing a set of compatible polynomials over $s$-inversion sequences, Savage and Visontai proved this conjecture in 2013. Using matrices preserving interlacing properties of nonnegative polynomial sequences, Bränden also established the real-rootedness of $D_n(x)$. Combining Hermite-Biehler theorem and a result of Borcea and Brändén on Hurwitz stability, Yang and Zhang gave another proof of the real-rootedness of $D_n(x)$. By constructing half Eulerian polynomials of type $D$, Hyatt reproved Brenti's conjecture. As originally suggested by Brenti in 1994, it is possible that the real-rootedness of $D_n(x)$ may be established by using a more precise knowledge of the location of zeros of the types $A$ and $B$ Eulerian polynomials. In this paper, we add more details to the first proof of the real-rootedness of $D_n(x)$ that was provided by the author in 2012, which yields the half interlacing property among the types $A,B$ and $D$ Eulerian polynomials.

Aurore Guillevic, Simon Masson

In 2021, Masson, Sanso, and Zhang introduced the Bandersnatch curve associated to the BLS12-381 pairing-friendly curve, an elliptic curve designed for zero-knowledge proofs requiring circuits with a curve arithmetic. This type of curve is useful for privacy-preserving protocols, and more generally for succinct validity proof using pairing-based SNARKs. An embedded curve is defined over a field whose order is the group order of its associated curve. In this way, the pairing-friendly curve is used to express a zero-knowledge proof (such as a SNARK) of a statement taking place on the embedded curve. Contrary to the previous embedded curves (such as CØCØ, JubJub), Bandersnatch was built with the complex multiplication (CM) method, in order to ensure a very small discriminant (-8, whose magnitude is small), and thus efficient scalar multiplication thanks to the GLV technique. The algorithm provided by Masson, Sanso, and Zhang for searching this type of curves requires computation of Hilbert class polynomials, making the search of curve slow. It was not known whether Bandersnatch was an exceptional curve or whether comparable curves exist, of larger discriminants. This paper highlights the technicalities of the CM method already in use in the 90s to generate curve parameters of chosen order. This old technique allows revisiting the curve search of Bandersnatch, providing a dramatic speed-up improvement. This paper presents two algorithms: one to generate embedded elliptic curves of SNARK-friendly elliptic curves, with a variable discriminant; a second to generate families (parameterized by polynomials) with a fixed discriminant. When the (negative) discriminant is -3 modulo 4, it is possible to obtain a prime-order curve, and form a cycle. To illustrate this, we apply the technique first to generate more embedded curves like Bandersnatch with BLS12-381, such as a curve of discriminant -6673027, defining a plain twist-secure cycle. We also comment on the scarcity of Bandersnatch-like CM curves, and recall that with this generic algorithm, it is only a question of core-hours to find them. Second, we show the link between a paper of Ben Smith in 2015 and the work of Dai, Lin, Zhao, and Zhou in 2023, obtaining prime-order parameterized families of embedded curves of fixed discriminant, such as -3 for BLS and KSS18 curves. With KSS16 curves, the discriminant -4 is also possible (the curve has an even order). The technique can work with any KSS, Scott–Guillevic, Gasnier–Guillevic, or other fixed-discriminant parameterized family of pairing-friendly curves. This paper provides a more general point of view on embedded curves such as Bandersnatch, putting into perspective the works of Masson, Sanso, and Zhang, and Sanso and El Housni. The Python/SageMath scripts are available at https://gitlab.inria.fr/zk-curves/cm-embedded-curves/.

Alexander Temerev, Alessio Doria

We solve Bellman's lost-in-a-forest problem for the golden gnomon $G$, the isosceles triangle with equal sides $1$ and apex angle $108^\circ$: the shortest curve guaranteed to reach the boundary of $G$ from an unknown starting position and heading is a symmetric seven-piece path of segments, circular shoulders, and tangents, of exactly determined length $C=1.282676025459\ldots$. To our knowledge, this is the first proved exact optimum for an isosceles triangle whose base angle is below $45^\circ$. The curve's parameters come from one isolated quartic root, and $C$ is transcendental. Equivalently, $C^{-1}G$ is the smallest homothetic golden-gnomon cover of all unit arcs. The proof introduces a balanced support calibration: one weighted family of escape inequalities, built on the linear relation among the triangle's three normals, exactly saturated by the candidate, through eighteen exact support windows, and confronting every shorter competitor at once. Aggregation along the normal fan compresses the calibration to a finite zero-sum family of supported vectors; summation by parts then bounds its total by path length whenever the running suffix balance, the ledger, stays in the unit disk. A local two-gap surgery and cyclic bitonicity force a shortest hypothetical counterexample into exactly the temporal order the ledger tolerates. Lean 4 verifies the two finite algebraic certificate families and the reusable discrete ledger identities and bounds.

Kyle Clouthier

AI now generates mathematics, code, and claims faster than anyone can review them; the limiting resource is no longer generation but trust. The honest response to "I don't trust it" is not "trust me" — it is "here is the check; run it." This deposit is a working demonstration of that response, run on the most scrutinized AI-math result of 2026: the July 2026 counterexample to the 87-year-old Jacobian Conjecture announced by Levent Alpöge with an AI as collaborator. A human directed Claude Code (Opus 4.8) as the proposer, with every mathematical claim compiled and machine-checked by Attestral, a verifier that signs an ed25519 certificate only when its own checker passes. The proposer cannot certify; the adjudicator has no stake in the proposer being right. The output is proof-carrying rather than model-asserted. Working only from the public polynomial list, the loop: independently verified the counterexample (det(JF) ≡ −2 exactly, a rational triple collision); reverse-engineered its mechanism (a non-nilpotent, degree-3 étale endomorphism — outside the classical nilpotent search space); found its hidden cubic (a three-cube-root Cardano fiber) and built an infinite tower of derived counterexamples; mapped the surrounding z-linear construction space (fold-parity obstruction, uniqueness skeleton); proved its natural four-dimensional generalization obstructed at every compensator degree in the Lean kernel; caught three of its own errors mid-run — including a finite-field prime silently collapsing to p = 3 — and discarded them; and reported an honest wall on the nilpotent normal form. Days later the same loop, unchanged, verified the counterexample to the Gaussian Moments Conjecture (Long, arXiv:2607.18186) posted in the same wave. Every claim carries a certificate any reader can re-verify offline: 20 Lean 4 kernel proofs (Mathlib, axiom-audited) for the load-bearing theorems and 23 exact-symbolic certificates (including the Gaussian-Moments companion) for the exploratory identities — two tiers, never blurred. The artifact bundle contains all 43 signed certificates, the Lean sources, the published verification key, and a standalone verifier needing only Python and pynacl: python verify_all.py → 43/43 certificates verified offline, ALL VALID. Scope, stated plainly: we verify and classify; the counterexample is Alpöge's. Certificates settle correctness only; one structural overlap is credited (Shaska, arXiv:2607.20210); no progress is claimed on the still-open plane (ℂ²) case. Interactive companion: https://simgen.dev/attestral/jacobian-counterexample/

Liu Ganqin, Hao Cheng, Georgios Fotiadis, Jipeng Zhang · 5 authors

The BLS digital signature scheme, in particular its instantiation with the BLS12-381 curve, has become a cornerstone of modern blockchain protocols such as Ethereum Proof-of-Stake, due to its unique and attractive characteristics (e.g., support for non-interactive signature aggregation). Recently, Cheng et al. (CHES 2025) demonstrated that the enormous Single-Instruction-Multiple-Data (SIMD) computing power of the Intel AVX-512 extensions, when combined with carefully-designed vectorization strategies, can be effectively leveraged to speed up the computation of the optimal ate pairing on BLS12-381, a major component of BLS. This naturally raises the question of whether such SIMD-parallel processing can be exploited more extensively to benefit the entire BLS signature scheme. The present paper answers this question positively by presenting a highly SIMD-optimized BLS implementation using Intel AVX-512, especially the AVX-512IFMA instructions. In order to harness AVX-512 more efficiently for the performance-critical operations of BLS, we explored a wide range of optimization options, including various formulas and vectorization granularities for elliptic curve arithmetic operations, scalar multiplication, and hashto- curve, as well as the fine-tuning and flexible use of different implementations of the finite-field arithmetic. Benchmarking results collected on an Intel Core i3-1005G1 (“Ice Lake”) CPU show that our vectorized BLS software using AVX-512 is at least 1.57 times faster than an x64 assembly implementation of the widely-used blst library

Muhammed Ismail

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.

김순채, Taewoon Kang, Sangwon Shin, Taeweon Suh · 6 authors

Zero-knowledge proofs (ZKPs) are emerging as a core technology for privacy-preserving computation. Despite steady progress in protocol and algorithm design, generating these proofs remains computationally intensive, driving growing interest in hardware acceleration for kernels such as number-theoretic transform (NTT) and multi-scalar multiplication (MSM). Among them, the sumcheck protocol offers a compelling alternative with O(n) prover complexity compared to O(nlog n) for NTT-based approaches, yet our analysis reveals its execution is fundamentally memory-bound, with severely underutilized compute resources. This characteristic demands a memory-centric acceleration strategy, in contrast to compute-centric approaches of prior work.

Amalan Joseph Antony, Kunwar Singh

No abstract is available for this record.

CARLES MARÍN MUÑOZ

A machine-checked, sorry-free formalization, in Lean 4 over Mathlib, of Sturm's theorem (1829): for a squarefree real polynomial p and an interval (a,b] whose endpoints are not roots, the number of distinct real roots of p in (a,b] equals V(a) − V(b), where V(x) is the number of sign changes of the Sturm sequence p, p′, −(p mod p′), … evaluated at x (zeros discarded). No root is ever located; two integers are subtracted. The mathematics is entirely classical and the result has been formalized before in other systems (Coq, by Cohen, within the construction of the real algebraic numbers; Isabelle/HOL, by Eberl, and in the Sturm–Tarski form by Li and Paulson; and HOL Light). To the best of the author's knowledge — based on searches of Loogle and Mathlib in June 2026 — this is the first proof of Sturm's theorem in Lean; it is a first-in-Lean and not a first-in-any-system. The contribution is therefore the formalization itself together with its reusable machinery: a small theory of sign variation, an inductive flank-reduction relation (FlankReduce) that decouples the chain's combinatorics from its algebra, and the local-to-global passage from a single root crossing to the interval count. A by-product is that Mathlib's existing count of coefficient sign variations (Descartes' rule, Polynomial.signVariations) and the count used here are, after unfolding, the same function — so the toolkit transfers verbatim to Descartes. The headline theorem Sturm.sturm depends only on the three standard axioms propext, Classical.choice, Quot.sound; no native_decide and no custom axiom. The whole proof is a single file (Sturm.lean, about 1,220 lines, ~60 declarations) depending on Mathlib alone. Scope, stated plainly: the theorem is proved for squarefree p over the reals; the passage to p/gcd(p,p′) for arbitrary polynomials is not formalized here. English and Spanish editions are included. Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility, and the Lean kernel — not the assistant — certifies the proofs.

Marc Guzmán Albiol

(English) The accelerated adoption of digital services has highlighted the need for trust-minimized computation, where parties can verify the correctness of computations without re-executing them or revealing sensitive data. Zero-knowledge proof systems, including SNARKs and STARKs, provide cryptographic guarantees of correctness, privacy, and succinct verifiability, enabling applications in scalable blockchains, privacy-preserving identity systems, and verifiable federated learning. This thesis addresses key inefficiencies in constraint-based zero-knowledge proof systems at the arithmetization layer. The research focuses on two complementary problems: optimizing binary comparisons within Rank-1 Constraint Systems (R1CS), and extending the expressiveness of STARKs through an Extended Algebraic Intermediate Representation (eAIR). The first contribution presents a weighted accumulation method for implementing strict binary comparisons in R1CS. Traditional approaches generate a large number of constraints due to the lack of native comparison and control-flow operations in the R1CS model, forcing costly bit-by-bit decompositions and creating performance bottlenecks. The proposed weighted accumulation method significantly reduces constraint overhead without compromising system security or correctness, achieving substantial efficiency improvements over the lexicographic approach. The second contribution introduces the eSTARK protocol, which extends standard STARKs by enabling the concise handling of complex constraints such as lookups, permutations, and copy constraints. These operations are difficult to encode efficiently in standard AIR. The eSTARK protocol integrates vector commitment arguments and polynomial optimizations, providing a flexible and user-friendly framework for representing a broader class of computations without introducing unnecessary arithmetization overhead. Both contributions address practical limitations of current zero-knowledge proof systems. The first focuses on reducing constraint complexity for common operations, while the second expands the expressiveness of the proof system itself. Together, they demonstrate the importance of arithmetization-level optimizations for improving the efficiency and usability of zero-knowledge proofs. (Català) L’adopció accelerada de serveis digitals ha posat en relleu la necessitat de computació amb confiança mínima, on les parts poden verificar la correcció dels càlculs sense haver de tornar-los a executar ni revelar dades sensibles. Els sistemes de proves de coneixement zero, incloent-hi SNARKs i STARKs, ofereixen garanties criptogràfiques de correcció, privacitat i verificabilitat concisa, permetent aplicacions en blockchains escalables, identitat preservant la privacitat i aprenentatge federat verificable. Aquesta tesi aborda les principals ineficiències en els sistemes de proves ZK basats en restriccions a la capa d’aritmetització. La recerca se centra en dos problemes complementaris: optimitzar les comparacions binàries dins dels Rank-1 Constraint Systems (R1CS) i ampliar l’expressivitat dels STARKs mitjançant una Representació Intermèdia Algebraica Estesa (eAIR). La primera contribució presenta un mètode d’acumulació ponderada per implementar comparacions binàries estrictes en R1CS. Els enfocaments tradicionals generen un gran nombre de restriccions a causa de la manca d’operacions natives de comparació i de control de flux en el model R1CS, obligant a descomposicions costoses bit a bit i creant colls d’ampolla en el rendiment. El mètode d’acumulació ponderada proposat redueix de manera significativa la sobrecàrrega de restriccions sense comprometre la seguretat o la correcció del sistema, aconseguint millores substancials d’eficiència respecte a l’enfocament lexicogràfic. La segona contribució introdueix el protocol eSTARK, que amplia els STARKs estàndard permetent la gestió concisa de restriccions complexes com ara lookups, permutacions i restriccions de còpia. Aquestes operacions són difícils d’encodear de manera eficient en l’AIR estàndard. El protocol eSTARK integra arguments de compromís vectorial i optimitzacions polinòmiques, oferint un marc flexible i fàcil d’utilitzar per representar una classe més àmplia de càlculs sense introduir sobrecàrrega d’aritmetització innecessària. Totes dues contribucions aborden limitacions pràctiques dels sistemes de proves de coneixement zero actuals, amb la primera centrada en reduir la complexitat de restriccions per a operacions comunes i la segona en expandir l’expressivitat del sistema de proves en si. Conjuntament, demostren la importància de les optimitzacions a nivell d’aritmetització per millorar l’eficiència i la usabilitat de les proves de coneixement zero. (Español) La adopción acelerada de servicios digitales ha puesto de relieve la necesidad de computación con confianza mínima, donde las partes pueden verificar la corrección de los cálculos sin tener que volver a ejecutarlos ni revelar datos sensibles. Los sistemas de pruebas de conocimiento cero, incluyendo SNARKs y STARKs, ofrecen garantías criptográficas de corrección, privacidad y verificabilidad concisa, permitiendo aplicaciones en blockchains escalables, identidad preservando la privacidad y aprendizaje federado verificable. Esta tesis aborda las principales ineficiencias en los sistemas de pruebas ZK basados en restricciones a la capa de aritmetización. La investigación se centra en dos problemas complementarios: optimizar las comparaciones binarias dentro de los Rank-1 Constraint Systems (R1CS) y ampliar la expresividad de los STARKs mediante una Representación Intermedia Algebraica Extendida (eAIR). La primera contribución presenta un método de acumulación ponderada para implementar comparaciones binarias estrictas en R1CS. Los enfoques tradicionales generan un gran número de restricciones debido a la falta de operaciones nativas de comparación y de control de flujo en el modelo R1CS, obligando a descomposiciones costosas bit a bit y creando cuellos de botella en el rendimiento. El método de acumulación ponderada propuesto reduce de manera significativa la sobrecarga de restricciones sin comprometer la seguridad o la corrección del sistema, logrando mejoras sustanciales de eficiencia respecto al enfoque lexicográfico. La segunda contribución introduce el protocolo eSTARK, que amplía los STARKs estándar permitiendo la gestión concisa de restricciones complejas como lookups, permutaciones y restricciones de copia. Estas operaciones son difíciles de codificar de manera eficiente en el AIR estándar. El protocolo eSTARK integra argumentos de compromiso vectorial y optimizaciones polinómicas, ofreciendo un marco flexible y fácil de usar para representar una clase más amplia de cálculos sin introducir sobrecarga de aritmetización innecesaria. Ambas contribuciones abordan limitaciones prácticas de los sistemas de pruebas de conocimiento cero actuales, con la primera centrada en reducir la complejidad de restricciones para operaciones comunes y la segunda en expandir la expresividad del sistema de pruebas en sí. Conjuntamente, demuestran la importancia de las optimizaciones a nivel de aritmetización para mejorar la eficiencia y la usabilidad de las pruebas de conocimiento cero.

Adiwena Putra, Cuong Manh Duong, Anh Quang Pham, Joo-Young Kim

Zero-knowledge proofs (ZKP) allows a prover to convince a verifier of computational correctness without revealing private data, ensuring both privacy and verifiability. However, proof generation is highly compute-intensive, dominated by polynomial (POLY) and elliptic-curve (EC) operations. These workloads pose two key challenges for hardware acceleration: (1) efficiently supporting diverse large-precision modular multiplications, and (2) maintaining high utilization across workloads that dynamically shift between POLY and EC stages. Existing reconfigurable accelerators address these issues only partially, remaining limited in precision scalability, algorithmic flexibility, and resource efficiency. To overcome these limitations, we propose ZK-Flex, a flexible and scalable software-hardware co-designed framework for accelerating ZKP proof generation. The software layer incorporates POLY and EC optimizers that reduce computation through hardware- and workload-aware algorithmic choices, while the hardware integrates TCore, a Toom-Cook-based multi-precision core with a flexible NoC and a linked-list memory mechanism that improves parallelism under limited memory capacity. Across representative ZKP benchmarks, ZK-Flex achieves 5 to 11 times speedup and up to 3.8 times higher area efficiency over the state of the art, establishing a new foundation for high-performance, reconfigurable ZKP acceleration.

Leo Noel, Thomas Plantard

No abstract is available for this record.

Ruwei Huang, Xiaolong Tang, Junjie Wang, Xuezheng Qin

Polynomial multiplication serves as a fundamental computational primitive in modern cryptography–including fully homomorphic encryption and zero-knowledge proofs –as well as in digital signal processing. Its performance optimization has become increasingly critical amid the rapid development of privacy-preserving computation and blockchain technologies. To address the limitations of traditional algorithms in meeting the demands for high throughput and low latency, this study proposes a high-performance polynomial multiplication accelerator based on the collaborative optimization of GPU-NTT and the Karatsuba algorithm. The method deeply integrates the asymptotically optimal complexity of NTT with the constant-factor efficiency of Karatsuba at moderate scales, and fully exploits the parallel computing power of GPUs to construct a modular, multi-stage pipelined acceleration framework. The divide-and-conquer nature of the Karatsuba algorithm is leveraged for coarse-grained parallelism, splitting large polynomial multiplications into subproblems handled by GPU thread blocks in parallel, while each subproblem is solved with fine-grained parallelism using GPU-accelerated NTT kernels. An innovative zero-padding strategy is introduced to enhance the generality of the NTT kernels, and shared memory caching is employed to alleviate GPU memory bandwidth bottlenecks. Experimental results on the NVIDIA RTX 4060 GPU demonstrate that the proposed method achieves a stable speedup of 1.43 \(\times \) to 1.49 \(\times \) over the baseline GPU-NTT for lower-dimensional polynomials, and outperforms the KNTT algorithm by up to 2.44 \(\times \) for higher dimensions (e.g., \(\log _2 n = 14\) ), showing superior scalability and robustness. Kernel execution time analysis further confirms that the method benefits from efficient kernel fusion and balanced workload distribution, which effectively avoids pipeline stalls and ensures high-throughput execution. This research provides a significant performance optimization solution for the practical deployment of advanced cryptographic technologies such as FHE and ZKP.

Hosny Abo Emira, Ayman Mohamed, Abdelrahman Elsayed, Mohamed Mostafa Ali · 5 authors

Zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARKs) allow for elegant, privacy-preserving validation of computations. PLONK, a subclass of the zk-SNARKs, is certainly useful, but its complex interactions with permutation arguments, lookup tables, and blinding, among other considerations, make the protocol difficult to follow, let alone understand. This paper describes a framework centered around the core components of zk-SNARKs. In particular, we detail the construction of arithmetic gate constraints, representation of witness polynomials, and the Kate-Zaverucha-Goldberg (KZG) commitment scheme. By removing permutation proofs, lookup, and blinding, we aim to simplify the pedagogy of zk-SNARKs and preserve their essential properties of soundness and completeness. We describe a Python module from the ground up that demonstrates the generation and validation of proofs in a PLONK-modified zk-SNARK. We validate the framework and its foundations with a benchmark of a module generating and validating proofs in a PLONK-modified zk-SNARK. We validate the module against a circuit of 1,000 gates and demonstrate that the system correctly rejects all invalid witnesses. We illustrate the expected asymptotic behavior, with a pro tor of tight the module is quasi-linear, and verification, tight. We justify the foundations of the module and describe tight with zero private inputs. We have also bridged the gap between abstract zk-SNARK theoretical arguments and their practical implementation and research. We have provided a simple, empirically grounded mechanism that describes the key components of PLONK. We have done this in such a way that researchers, developers, and teachers can build on this base module and create production-ready systems without the abstraction.

Miguel Isabel, Enric Rodríguez-Carbonell, Clara Rodríguez-Núñez, Albert Rubio

Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.

Andrés Sebastián Pirolo

Abstract Multi-Scalar Multiplication (MSM) is the primary computational bottleneck in zero-knowledge (ZK) proof generation for decentralized networks. This research accelerates MSM by solving the memory bandwidth constraints inherent in high-dimensional elliptic curve cryptography. We introduce Modular Hypercube Chunking, a novel microarchitectural approach that partitions high-dimensional algebraic precomputations into smaller, orthogonal blocks. Specifically, we divide a 12-dimensional workload into three separate 4D hypercubes, restricting the entire memory footprint to 31.1 KB. This geometric partitioning ensures perfect residency within the ultra-fast L1 cache of modern processors. By employing shared doubling across these blocks, the algorithm processes twelve scalars simultaneously with a single elliptic curve duplication, bypassing slow RAM access entirely. Empirical evaluations conducted on an ARM Snapdragon 8 Gen 2 mobile processor demonstrate a peak 5.37× speedup compared to optimized sequential baselines, reducing the computational cost to 18.44 microseconds per scalar. These findings prove that geometric data partitioning within strict L1 cache boundaries significantly outperforms traditional arithmetic-heavy optimizations. The implications of this work provide a highly scalable architecture capable of executing server-grade ZK-Rollup proof generation on resource-constrained edge devices, while establishing a highly efficient blueprint for future multicore hardware accelerators. Furthermore, initial stress-tests of a 12D monolithic architecture (68 MB footprint) yielded an anomalous 8.88× peak speedup. This finding reveals a novel sparse-access memory optimization path, which we introduce as an open architectural challenge.

changzheng zhou, ziqing zhou

The modular invariance and automorphism group rigidity of vertex operatoralgebras provide a profound mathematical foundation for constructing novel postquantum cryptographic systems. However, a significant theoretical and engineeringgap exists between mathematical theorems and deployable cryptosystems. Thispaper does not propose new cryptographic protocols but rather systematicallyexamines the core challenges encountered in engineering vertex operator algebracryptography: the discrete selection of parameter spaces and their quantitativerelationship with security strength, the computational resource requirements ofcandidate algebraic families (lattice vertex operator algebras, WZW models, andmoonshine vertex operator algebras), the assessment of security boundaries underquantum attack models, and the practical overhead of auxiliary mechanisms suchas zero-knowledge proofs. The objective is to provide a clear problem inventoryand a feasibility analysis framework for future research, rather than to claim anyimmediately usable security parameters. The article concludes by summarizing thecurrent technology readiness levels and identifying the key breakthroughs requiredto advance from a theoretical framework toward a practical system.

Florian Krieger, Christian Dobrouschek, Florian Hirner, Sujoy Sinha Roy

We present the first high-performance SIMD software implementation of Spielman codes for their use in polynomial commitment schemes and zero-knowledge proofs. Spielman codes, as used in the Brakedown framework, are attractive alternatives to Reed-Solomon codes and benefit from linear-time complexity and field agnosticism. However, the practical deployment of Spielman codes has been hindered by a lack of research on efficient implementations. The involved costly finite-field arithmetic and random memory accesses operate on large volumes of data, typically exceeding gigabytes; these pose significant challenges for performance gains. To address these challenges, we propose several computational and memory-related optimizations that together reach an order-of-magnitude performance improvement in software. On the computation side, we propose SIMD optimizations using the AVX-512-IFMA instruction set and introduce a lazy reduction method to minimize the modular arithmetic cost. On the memory side, we implement a cache-friendly memory layout and a slicing technique, which exploit the CPU memory hierarchy. Finally, we present our multithreading approach to improve throughput without saturating memory bandwidth. Compared to prior Spielman software, our optimizations achieve speedups of up to 21.9x and 20.6x for single- and multi-threaded execution, respectively. In addition, instantiating our software with 64 threads on a high-end CPU even outperforms a recent FPGA accelerator by up to 4.3x for small and mid-sized polynomials. Our improvements make Spielman codes competitive with well-optimized Reed-Solomon codes on software platforms.

Nobuki Fujimoto

Adds a fourth rigorous anchor to the Rei-AIOS D-FUMT8 logic by exhibiting each p-adic completion Q_p as a distinct FLOWING-instance of the same rational. Empirical: 23/25 (92 percent) of representative rationals are FLOWING under the standard prime list. Formal: 11 zero-sorry Lean 4 theorems including two FLOWING-witness inequalities (dfumt8MarkNat 2 27 != dfumt8MarkNat 3 27 and dfumt8MarkNat 13 247 != dfumt8MarkNat 2 247) proved by native_decide via Mathlib padicValNat. Together with Papers 69 (Schnorr), 75-76 (QuTiP), and 77 (LeanDFumt), this completes a QUADRUPLE ANCHOR for D-FUMT8 spanning computability, physics, proof theory, and number theory. To our knowledge the first explicit p-adic ↔ eight-valued logic mapping.

Alexandre Linhares

We present a formal verification of Wolstenholme's theorem -- $\binom{2p}{p} \equiv 2 \pmod{p^3}$ for prime $p \geq 5$ -- in Lean~4 with Mathlib. The proof proceeds by expanding the shifted factorial product $\prod_{k=1}^{p-1}(p+k)$ to second order in $p$, identifying the quadratic coefficient as the second elementary symmetric product, and showing its divisibility by $p$ via power sum vanishing in $\mathbb{Z}/p\mathbb{Z}$. The formalization comprises nine lemmas across approximately 800 lines of Lean, with zero \texttt{sorry} declarations. To our knowledge, this is the first formal verification of Wolstenholme's theorem in Lean~4. The proof was discovered through a collaboration between a relational analogy engine for theorem proving and human-directed formalization.

Moriba Kemessia Jah

We introduce the Theory of Epistemic Abductive Geometry (TEAG), a framework for non-Bayesian inference grounded in admissible-support contraction under possibility theory. The central object is the TEAG quintuple \( \mathcal{E} = (H, \pi, \{H_\alpha\}_{\alpha\in(0,1]}, C, A) \), where evidence acts by contracting the geometry of admissible hypotheses rather than redistributing probabilistic belief mass. The falsification boundary is a tropical variety — exactly. Under the log-admissibility transformation \( \Phi(h) = -\log\pi(h) \), the canonical TEAG conjunctive update becomes tropical addition in the max-plus semiring: \( \Phi^+(h) = \Phi^-(h) \oplus \psi(h) = \max\!\bigl(\Phi^-(h),\,\psi(h)\bigr), \) where \( \psi(h) = -\log\kappa(y\mid h) \) is the surprisal of hypothesis h under observation y. The falsification boundary is the tropical variety of this polynomial: \( \mathcal{F} = \bigl\{h \in H : \Phi^-(h) = \psi(h)\bigr\}. \) This is the exact locus dividing surviving from falsified hypotheses: h is falsified if and only if \( \psi(h) > \Phi^-(h) \); it survives if and only if \( \Phi^-(h) \geq \psi(h) \). Within the class of possibility-theoretic recursive inference systems, this is, to the best of our knowledge, the first exact algebraic expression of Popper's falsification criterion: the boundary is the zero set of a tropical polynomial, determined entirely by the geometry of the prior impossibility and current surprisal fields. Main results. 1. Epistemic Contraction Theorem. Contraction is tropical addition: \( \Phi^+ = \Phi^- \oplus \psi \). Posterior α-cuts satisfy \( H_\alpha^+ = H_\alpha^- \cap E_\alpha(y) \): geometric intersection, not belief redistribution. The falsification boundary is the tropical variety \( \mathcal{F} \). 2. Possibilistic Cramér–Rao Bound (PCRB} For any filter in the class \( \mathcal{F} \) of epistemically admissible, contraction-based recursive estimators satisfying Axioms 2.1–2.5: \( \mathcal{E}_{\pi,k|k} \geq \mathcal{E}_{\pi,k|k-1} + \tfrac{n}{2}\log(1-I_k) \), where \( I_k \) is the Choquet integral of per-hypothesis surprisal against the prior possibility capacity. Within this class, the ESPF [28] is the unique filter achieving this bound with equality, and is therefore the unique minimax-entropy-optimal set-based recursive estimator under bounded epistemic uncertainty. 3. Tropical Hamilton–Jacobi structure (summary). The TEAG update is structurally consistent with a tropical Lagrangian \( L = T - V \), Legendre transform to a tropical Hamiltonian equal to the surprisal field, and a Hamilton–Jacobi equation whose solution is the tropical addition rule. The Euler–Lagrange equations on the epistemic manifold yield geodesic motion with explicit Levi–Civita connection and Christoffel symbols. This structure is interpretive and consistent with the axioms; full derivations are in the companion paper [31]. Taken together, this structure admits a precise interpretation: the TEAG update rule is a max-plus dynamical system whose governing equations have the same algebraic form as the Hamilton–Jacobi equations of classical mechanics, instantiated on hypothesis space rather than physical space. 4. Gaussian collapse. Probability theory is the collapse limit of TEAG as epistemic width \( W \to 0 \): Choquet converges to Lebesgue, the ESPF recovers the Kalman filter, and \( \mathcal{E}_\pi \to \tfrac{1}{2}\log\det\Sigma + \mathrm{const}(n) \). Probability is earned by evidence, not assumed. Epistemic neutrality and knowledge-system synthesis. Because TEAG's axioms require only a hypothesis space, a possibility field, and a contraction operator — not a probability measure, a likelihood function, or a frequentist grounding — heterogeneous knowledge systems can each instantiate the TEAG quintuple independently. Their joint admissible support intersection is the locus of coherence: the set of hypotheses neither system has falsified. No transformation of one system into the other's representational primitives is required. The composition theory (Section 6) formalizes the coupling architecture. Four instantiations provide the unifying structure: the ESPF [28] for recursive state estimation; the Geometry of Knowing [29] for measure-theoretic collapse; the minimax-entropy optimality proof [30]; and the Possibilistic Language Model (PLM, forthcoming [32]).

Ayumi Ohno, Kotaro Shimamura, Shinya Takamaeda-Yamazaki

Multi-Scalar Multiplication (MSM) is a primary computational bottleneck in modern cryptographic applications, especially zero-knowledge proofs. The Pippenger algorithm parallelizes MSM by decomposing it into numerous elliptic curve point additions (PADDs), but accelerating these operations on novel hardware like the Versal ACAP presents a significant challenge. This work explores the acceleration of PADDs on the Versal ACAP’s spatial array of 400 AI Engines (AIEs). While the SIMD-VLIW architecture of AIEs is ideal for the multiplication-heavy workloads in PADD, the complex 377-bit modular arithmetic, particularly carry propagation, demands architecture-aware optimization. We propose two key contributions: (1) algorithmic optimizations for carry propagation employing a carry-save-like technique to exploit VLIW and SIMD capabilities, and (2) a comparison of spatial mapping strategies and modular reduction algorithms to enhance intra- and intertask parallelism. Our approach achieves 567× speedup over the integrated CPU on the AIE evaluation board, utilizing 51.1% of the theoretical memory bandwidth.