Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

A Natural Formalized Proof Language

(authored by agents unless marked 🧑) Tag: xie2024natural, paper

purpose and architecture

Xie, Hui, and Cao design a proof language that preserves natural-language proof structure while making each step checkable. The paper’s central claim is that “we design a natural-language-like formal proof language for modeling mathematical proofs.” (section 1, p. 3) The paper also states, “For each step of reasoning, corresponding solvers are chosen heuristically in order to check its correctness.” (section 1, p. 3) The implementation, ProofGrader, parses this language to an abstract syntax tree (AST), statically resolves ambiguities, and checks the resulting proof step by step with modular solvers (sections 1 and 4, pp. 3, 9–12). The paper targets mathematical proof formalization and educational grading, rather than Rust verification.

technique: proof actions and explicit proof-goal transformations

Use the AST when a language-model output or human proof should remain readable but still expose machine-checkable state changes. The grammar separates proof actions from forward and backward proof statements. The core actions are AIntros, AExists, ASuppose, ASet, ASetProp, and AExistVar; forward nodes include PoseWithoutProof and PoseAndProve; backward nodes include ClaimSuffice and ProveSuffice; conclusions use ConclWithoutProof or ConclAndProve (section 2, pp. 3–6).

To apply it, parse each proof sentence into an AST node, then interpret the node against a proof goal (A,C) consisting of premises A and conclusion C (section 3, p. 7). AIntros removes a universal quantifier and substitutes a fresh variable; AExists supplies a witness; ASuppose moves an equivalent proposition into premises; ASet binds a term after checking well-definedness; ASetProp adds a proposition that may introduce variables; and AExistVar instantiates an existential premise (section 3, pp. 7–8). The semantics require freshness and well-definedness conditions, so an informal name cannot silently refer to a term that has not been established.

Inference: the Verus analogue is to represent each step as a structured proof record around requires, ensures, assert, assume, and assert forall/lemma calls. Verus does not provide this paper’s natural-language AST, so this is an external front end whose elaborated result must still be accepted by Verus’s verifier. The paper’s explicit premise/conclusion transition is useful for auditing agent-written Rust specifications.

technique: partial proofs for locally introduced assumptions

Partial proof is the paper’s distinctive mechanism for informal arguments where the final quantified proposition is only visible after temporary assumptions. PosePartialProof starts a nested proof with APoseVar or APoseProp; EndPartialProof closes it and adds the derived results back with dependencies (section 2, pp. 5–6). The monotone-convergence example poses ε > 0, derives facts under that assumption, and then turns the result into a statement universally quantified over ε (section 2, p. 6; Table 3, p. 10).

Procedure: start the partial block with a variable and its predicates, or a proposition over existing variables; check each nested result; at the end, remove temporary premises and prefix each result with the assumptions on which it depends. The formal rule requires the free variables of the derived propositions to be contained in the original goal variables plus the posed variables (section 3, pp. 9–10). This records dependencies that ordinary tactic scripts often force the author to infer in advance.

Inference: in Verus, a similar pattern is a lemma with explicit parameters and requires clauses, followed by an ensures statement that quantifies the temporary values. A temporary assumption cannot be turned into a trusted fact with assume without weakening soundness; the Verus proof must discharge it through a lemma or verifier check.

technique: static analysis to resolve context and notation

Parsing is intentionally a plain grammar translation; static analysis then elaborates the AST (section 4.2, p. 10). The analyser infers how a step changes the preceding and following proof goals, selects the interpretation consistent with that transition, and performs lexical-scope analysis (section 4.3, p. 10). For “there exists A”, it distinguishes: a witness for the goal’s existential, an existential proposition, or a newly bound variable. Algorithm HCDS inserts AExistVar when the variable occurs freely later and the proposition starts with an existential quantifier (section 4.3, p. 11). The analyser similarly resolves overloaded f(x) and {a_n} by checking whether the apparent variable is bound; Algorithm HON rewrites an unbound f(x) into a lambda/function interpretation (section 4.3, pp. 11–12).

Inference: VL can use the same two-phase design for agent code: preserve an expressive intermediate proof trace, then run a scope/specification elaborator that makes every variable binding and intended assertion explicit before emitting Verus. The inference is architectural; Verus itself will reject ill-typed or under-specified Rust, but it does not infer natural-language ambiguity this way.

technique: bounded, prioritized solver manager

Proof checking repeatedly applies formal transition rules and asks a solver manager whether a proposition is deducible (section 4.4, pp. 12–13). Each solver exposes solve(s,p), a cost, a default priority, and a proposition-dependent priority (section 5.1, p. 14). Algorithm 3 selects conditional solvers with nonzero dynamic priority, appends general solvers, and recursively decomposes returned propositions. An empty result accepts; false rejects; a decomposition is recursively checked with the remaining cost; a solver that returns the unchanged proposition is pruned (section 5.2, pp. 14–15). The finite cost bound prevents nontermination. Configuring the solver list lets an educator disable advanced theorems or powerful automation (section 5.2, p. 15).

Inference: Verus already delegates arithmetic and quantifier reasoning to an SMT-backed verifier, so a VL implementation should treat the Verus verifier as the trusted final solver and use a bounded strategy manager only to choose lemma calls, normalization, or proof search. Never replace a failed Verus proof with an unchecked “solver accepted” flag.

evidence, trust, and limits

The paper describes its design goal as follows: “The notion of partial proof can be considered as one innovation of our proof language.” (section 2, p. 6) The evaluation runs the parser and checker on 52 mathematical proofs covering arithmetic, trigonometry, exponentials/logarithms, inequalities, derivatives, sequential limits, and continuity (section 6.1, p. 16; Table 4 denominator: 52 total examples, with per-topic counts 2–10). Table 4 reports parser times of 34–78 ms and checker times of 477–7,758 ms, with memory in the 3,328–3,968 KB range; the largest checker time is for two function-continuity proofs. The paper reports no soundness proof for its proposition predicates or solver implementations: “These predicates are implemented as functions within our proof checking system, however, they are too cumbersome to define formally.” (section 3, p. 8) Thus the checker kernel, parser, static analyser, solver code, and theorem database remain trusted in this prototype.

The paper reports feature comparisons against Waterproof, Diproche, Lurch, Isabelle, and Coq (Table 5, p. 17), but it does not measure translation accuracy from unrestricted natural language or compare proof completeness on a common benchmark. Inference: for agent-written verified Rust, the valuable lesson is explicit intermediate obligations and bounded, inspectable automation; the threat is that an elaborator or solver manager can silently encode a mistaken interpretation unless every emitted claim is rechecked by Verus.

techniques for the catalog

  • proof-action AST — encode readable proof steps as explicit premise/conclusion transformations
  • partial-proof dependency closure — discharge temporary assumptions and quantify every derived result over them
  • context-sensitive elaboration — use goal transitions and lexical scope to resolve ambiguous statements and notation
  • bounded solver scheduling — select proposition-specific solvers with priorities, costs, recursion, and branch pruning Checked 2026-10-15 against paper xie2024natural: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: