[challenge]: All in one: a native language for code + theorem + proof

Released by

Huanhai ZHOU, the Hong Kong University of Science and Technology (Guangzhou)

Contact email

albus.zhouhh@gmail.com

Method

Other

Challenge issue

The issue

Scientific computing has fast languages without theorems, and proof assistants without speed. Jax runs traced numerics at hardware speed but its type discipline cannot state a proposition; Lean 4 proves theorems but has no performant tensor runtime; Rust has a strict, feedback-rich type system with neither propositions nor numerics. Whoever wants both today builds a bundle — numerics in one language, proofs in another, glued by translation — and the bundle has a structural disease: the theorem and the executable denote different objects. The proof talks about a mathematical function defined in the prover's logic; the GPU runs a traced graph; the correspondence between them is checked by nobody. Two sources of truth.

The challenge: design a native language — a full language or a domain-specific language (DSL) — with design references to Jax, Rust, and Lean 4, that performs numerical computation and formal proof in one pass. One program that runs as fast as compiled Jax code and carries machine-checked theorems about the algorithm it executes. A DSL scoped to tensor programs qualifies, provided it meets the native criteria and the goals below. Explicitly not a bundle of existing languages, not a plugin, not a translation layer: a native type system, one kernel.

The target domain makes the one-pass requirement forced rather than aesthetic. In tensor-network algorithms the dominant error is truncation, and it is data-dependent — the singular values a particular run discards. A static proof cannot know them; a prove-it-afterwards bundle must re-verify against dumped data. Only a type system in which proofs can consume runtime values lets the same execution return the state together with a machine-checked bound on its own error.

What "native" means

Operational criteria — submissions are judged against these:

1. One kernel. A single core calculus and a single checker whose judgments carry three loads at once: shapes and indices (dependent types — what Jax fakes dynamically), resource and aliasing discipline (linear or affine modes in the spirit of Rust ownership, which is what makes in-place tensor updates safe), and propositions (an erasable universe of propositions, as in Lean).
2. One semantics. The term a theorem is about and the term that executes are the same object with one meaning. Compilation to machine code is part of the system's account, not an external extraction step taken on faith.
3. Erasure. Proofs vanish after type checking; the residual program is the loop nest an array compiler would emit — this is why matching Jax is possible at all. Runtime values that the specification needs (an accumulated error bound) are ordinary computation whose correctness was settled statically.
4. Axioms allowed, a second semantics banned. Linked kernels (BLAS/LAPACK, LLVM) may enter as typed primitives with axiomatized specifications declared inside the language. Every submission enumerates its trusted computing base (TCB): axioms plus linked components. Banned: any round-trip through another language's checker or runtime — emitting Lean and shelling out to check it, generating Python/Jax, translating between existing front ends.
5. Staging inside the theory. Just-in-time (jit) compilation is typed metaprogramming in the same calculus, not an external tracer. Automatic differentiation (AD) is an in-language program transformation whose rules carry proof obligations.

Required expressiveness: complex dense tensors, contraction/einsum, singular value decomposition (SVD) and QR, structured loops (scan), jit; gradients where Goal 2b is attempted.

Goal 1 (mandatory) — two separate deliverables

(1a) Plain MPS TDVP, fast and certified. Implement time evolution of matrix product states (MPS) by the time-dependent variational principle (TDVP) on ordinary dense tensors. Two requirements on the same program:

• Speed: wall-clock not slower than a reasonable jit-compiled Jax implementation of the same algorithm, on the same hardware with the same linked BLAS/LAPACK. The Jax baseline is part of the submission; its reasonableness is judged at review.
• Certification: the run emits a machine-checked accumulated error bound $\varepsilon$ at the level of algorithmic theorems in exact real arithmetic: each truncation carries its Eckart–Young certificate — keeping the largest $\chi$ singular values is the optimal rank-$\chi$ approximation, and the local error equals the discarded weight computed from this run's singular values — and the per-step errors compose into $\varepsilon$ through a checked triangle inequality. Produced in the same pass by the same compiled artifact, not by a separate verification process.
• Declared design freedom — floating point. The certification above is exact-arithmetic; rounding is assumed faithful (it sits roughly ten orders below typical truncation error). A submission may instead strengthen to floating-point-aware certification — the IEEE 754 model $\mathrm{fl}(a \circ b) = (a \circ b)(1+\delta)$ with $|\delta| \le u$, composed through the algorithm, with backward-stability axioms for linked kernels (the machinery exists: LAProof). Each submission states which convention it adopts.

(1b) Symmetric tensors as types. A separate deliverable, demonstrated on its own rather than entangled with the TDVP benchmark. Encode symmetry sectors (e.g. $U(1)$ charge conservation) in the type system so that:

• sector consistency of the whole program is checked before execution — an illegal fusion does not compile;
• zero blocks are eliminated by the compiler, justified by the conservation theorem;
• the fusion-category laws themselves — associativity of fusion and F-symbol consistency (the pentagon equation) — are stated and machine-checked in-language.

Prior art to beat: TensorKit.jl encodes sectors in Julia's parametric types, but enforcement happens at runtime dispatch along the executed path, and the category laws live in trusted, unit-tested library code. The native version certifies the laws and checks programs statically: typed bookkeeping becomes certified bookkeeping.

Goal 2 (choose one) — the formal system enhances computation

(2a) Lemma-driven compilation. At least one optimizer pass whose soundness is a machine-checked lemma in the language's own library — not a built-in pass trusted from the compiler. Verification: compile identical source with the pass off and on; report the wall-clock gain on a named many-body workload; the optimized build must beat the reasonable Jax baseline. The canonical instance is (1b)'s zero-block elimination — the speedup exists because a conservation theorem proves those blocks vanish, which a dense-tensor tracer structurally cannot know. (Precedent that rewrite-search beats compiler heuristics exists in equality saturation; the delta here is that every rewrite is a theorem.)

(2b) Derived automatic differentiation. Derivative rules are derived in-language from an enumerated, small set of primitive axioms plus calculus lemmas — chain and product rules as theorems — rather than a hand-written rule table. Verification: (i) the enumerated primitive list; (ii) a held-out composite function, e.g. one TDVP sweep, auto-differentiated with proof and matching finite differences at Jax-comparable speed; (iii) as showcase, the real-SVD gradient derived with its nondegeneracy hypothesis as a typed precondition — existing frameworks silently produce NaNs at degenerate singular values, whereas here the type demands the hypothesis. The complex-SVD gradient is explicitly optional: its gauge-phase obstruction is a research problem of its own.

There is a single bar — Goal 1 plus one of Goal 2. No tiers.

Natural extensions (not required)

• Two-sided certified ground-state intervals: a certified variational upper bound combined with a certified relaxation lower bound (cf. challenge #49) yields a machine-checked interval containing $E_0$.
• Certified Trotter budgets: splitting-error theorems instantiated with computed commutator norms — "$n$ steps suffice for accuracy $\varepsilon$", with proof.

Why this may lead to research output

• The triangle is unclaimed. SciLean derives AD rules by theorem-guided rewriting in Lean 4, far from Jax speed; Dex built fast typed arrays with no propositions; F*/Low* delivered proofs at hand-written-C speed for cryptography, without tensors or staging; TNLean is formalizing MPS theory with no execution story. Dependent proofs + Jax-speed tensors + one native kernel exists nowhere. A language meeting Goal 1 is a publishable programming-languages result and a working tool for computational physics at once.
• Agent-native design. The learning-curve ceiling that keeps humans away from Rust-plus-Lean-grade systems does not bind AI agents; what binds agents is feedback quality. A deliberately strict, rich type system with high-quality diagnostics is the agent's guidance signal — a language designed for AI-driven research and numerics, rather than adapted to it.
• Single source of truth, machine-checkable publication. Agentic publication proposals bundle paper, code, and environment — and prose and code remain two authorities. In this language the claim, its proof, and its execution are one artifact; papers and talks demote to human-digest views of it, and reviewing the formal claims reduces to running the kernel.

References

1. Jax — J. Bradbury et al., JAX: composable transformations of Python+NumPy programs (2018), github.com/jax-ml/jax.
2. R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer, RustBelt: securing the foundations of the Rust programming language, POPL 2018.
3. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, CADE-28 (2021).
4. SciLean — T. Skřivan, scientific computing in Lean 4, github.com/lecopivo/SciLean.
5. A. Paszke et al., Getting to the point: index sets and parallelism-preserving autodiff (Dex), ICFP 2021, arXiv:2104.05372.
6. J. Protzenko et al., Verified low-level programming embedded in F*, ICFP 2017, arXiv:1703.00053.
7. S. Lu, E. Tjoa, and J. I. Cirac, Multi-agent autoformalization of tensor network theory (TNLean), arXiv:2607.07857.
8. A. Kellison et al., LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs, ARITH 2023.
9. J. Haegeman et al., Time-dependent variational principle for quantum lattices, Phys. Rev. Lett. 107, 070601 (2011).
10. J. Haegeman et al., Unifying time evolution and optimization with matrix product states, Phys. Rev. B 94, 165116 (2016).
11. C. Lubich, I. Oseledets, and B. Vandereycken, Time integration of tensor trains, SIAM J. Numer. Anal. 53, 917 (2015).
12. M. Willsey et al., egg: fast and extensible equality saturation, POPL 2021, arXiv:2004.03082.
13. S. Lu and X.-L. Qi, Agentic publication protocol: an attempt to modernize scientific publication, arXiv:2606.27386.
14. TensorKit.jl — J. Haegeman, github.com/Jutho/TensorKit.jl.

No repository files, tests, or implementation entry points are named in the issue, so start by studying the stated native-kernel criteria and the cited Jax, Rust, Lean, and tensor-network references. Done means delivering Goal 1a and 1b plus either Goal 2a or 2b, with the required performance comparisons, machine-checked guarantees, and declared trusted computing base.