One binary operator eml(x,y)=exp(x)-ln(y) plus the constant 1 generates all elementary functions including sin, cos, sqrt, log, arithmetic operations, and constants e, pi, i.
The lean 4 theorem prover and programming language,
6 Pith papers cite this work, alongside 9 external citations. Polarity classification is still indexing.
6
Pith papers citing it
9
external citations · OpenAlex
years
2026 6representative citing papers
An LLM agent with Rocq backend automatically builds a verified RISC-V RV32I interpreter (1859 lines Rocq, 2848 lines extracted C++) that passes 265 tests and 12-hour fuzzing, while a Dafny backend fails.
Six Birds Theory defines agents as maintained theory objects with feasible policies that make counterfactual differences, operationalized via ledger feasibility, viability kernels, empowerment, and packaging maps, and tested in ring-world simulations showing distinct separations.
Formalizes line search methods, conditions, and Zoutendijk theorem in Lean 4 to support verified nonlinear optimization.
A reduced front-seed coherence package (WL, WR) plus one pentagon contraction recovers associator, pentagon, and bridge theorems, while explicit coordinatewise reify/reflect formulas are given for K-infinity, all Lean-4 formalized without axioms.
citing papers explorer
-
All elementary functions from a single binary operator
One binary operator eml(x,y)=exp(x)-ln(y) plus the constant 1 generates all elementary functions including sin, cos, sqrt, log, arithmetic operations, and constants e, pi, i.
-
Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
An LLM agent with Rocq backend automatically builds a verified RISC-V RV32I interpreter (1859 lines Rocq, 2848 lines extracted C++) that passes 265 tests and 12-hour fuzzing, while a Dafny backend fails.
-
To Throw a Stone with Six Birds: On Agents and Agenthood
Six Birds Theory defines agents as maintained theory objects with feasible policies that make counterfactual differences, operationalized via ledger feasibility, viability kernels, empowerment, and packaging maps, and tested in ring-world simulations showing distinct separations.
-
Formalization of Line Search Methods by Lean
Formalizes line search methods, conditions, and Zoutendijk theorem in Lean 4 to support verified nonlinear optimization.
-
Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
A reduced front-seed coherence package (WL, WR) plus one pentagon contraction recovers associator, pentagon, and bridge theorems, while explicit coordinatewise reify/reflect formulas are given for K-infinity, all Lean-4 formalized without axioms.
- Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers