NATP: Native Automated Theorem Proving in Rust

NATP brings automated proofs into ordinary Rust development through a typed API for mathematical sequence properties. Programmers state claims in Rust and check them alongside their tests. For identities involving concatenation and reversal of integer sequences, NATP automatically produces a proof or a concrete counterexample. The procedure uses signed-word normalisation, with soundness, completeness and a tight counterexample bound of two elements per input sequence formalised in Lean. A separate Lean checker validates exported evidence. The API distinguishes these proofs from bounded verification and SMT-assisted results. We measure decision, evidence construction and checking separately. Compact evidence reduces construction costs for valid identities by omitting the general backend’s diagnostic traces. Repository: https://github.com/NATPProject/natp