Formalizing Wu-Ritt Method in Lean 4

Dingkang Wang, Hao Shen, Junyu Guo, Lihong Zhi, Yuxuan Xiao

Pith reviewed 2026-05-10 08:40 UTC · model grok-4.3

classification 🧮 math.AC cs.LO

keywords Wu-Ritt methodcharacteristic setsLean 4formal verificationtriangular decompositionpolynomial systemszero decompositiontheorem proving

0 comments

The pith

Lean 4 formalizes the Wu-Ritt method and proves correctness of its algorithms for triangular decomposition of polynomial systems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper builds a machine-checked development of the Wu-Ritt characteristic set method inside Lean 4. It supplies definitions for polynomial initials, pseudo-division, pseudo-remainders, and ascending sets, then encodes algorithms that compute basic sets, characteristic sets, and zero decompositions while proving termination and correctness. The central result is a formal statement of the well-ordering principle that links any polynomial system to its characteristic set, together with a proof that zero decomposition writes the original zero set as a union of zero sets of triangular sets, excluding the zeros of the corresponding initials. A reader would care because the work turns a classical but hand-checked algebraic technique into a verified library that can underpin reliable computer-algebra tools and geometric theorem provers.

Core claim

We formalize the Wu-Ritt characteristic set method for the triangular decomposition of polynomial systems in the Lean 4 theorem prover. Our development includes the core algebraic notions of the method, such as polynomial initials, orders, pseudo-division, pseudo-remainders with respect to a polynomial or a triangular set, and standard and weak ascending sets. On this basis, we formalize algorithms for computing basic sets, characteristic sets, and zero decompositions, and prove their termination and correctness. In particular, we formalize the well-ordering principle relating a polynomial system to its characteristic set and verify that zero decomposition expresses the zero set of the o rig

What carries the argument

The characteristic set of a polynomial system, obtained through repeated pseudo-remainder reduction and the well-ordering principle, which supports the decomposition of the zero set into triangular components away from initial zeros.

Load-bearing premise

The Lean 4 formal definitions of initials, pseudo-remainders, and triangular sets exactly match the classical informal notions, with all case distinctions for termination and zero-set equivalence covered.

What would settle it

A concrete polynomial system for which the Lean-computed zero decomposition differs from the decomposition obtained by the classical Wu-Ritt procedure on the same input.

read the original abstract

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

They've delivered a full Lean 4 formalization of the Wu-Ritt method with termination and zero-decomposition proofs.

read the letter

The main point is that this paper has formalized the Wu-Ritt characteristic set method in Lean 4, complete with termination proofs and a verified statement about zero decomposition. They've done the core work well by defining the necessary notions—polynomial initials, pseudo-remainders, standard and weak ascending sets—and then coding up the algorithms for basic sets, characteristic sets, and the zero decomposition. The proofs of the well-ordering principle and the correctness of the decomposition as a union of triangular sets (away from initials) are included. This kind of formalization is genuinely useful because it turns an established but informal method into something that can be trusted in certified computations for engineering and math. What they did right is sticking to the classical definitions and using Lean's proof assistant to check everything. No invented entities or free parameters here; it's a direct formalization. The soft spots are limited. Since I only have the abstract to go on, I can't inspect the actual proof scripts for completeness on edge cases like division by zero or specific polynomial orders. But the claims match what one would expect from a careful formalization, so the risk seems low. The development appears sound internally. This is for people in the intersection of formal verification and algebraic geometry or computer algebra. Someone building tools for geometric theorem proving would find it relevant and could build on it. I'd recommend sending it for peer review. It's a concrete contribution that deserves a referee's time to verify the details and assess its usability.

Referee Report

0 major / 3 minor

Summary. The paper formalizes the Wu-Ritt characteristic set method in Lean 4 for triangular decomposition of polynomial systems. It defines core algebraic notions including polynomial initials, orders, pseudo-division, pseudo-remainders (w.r.t. a polynomial or triangular set), and standard/weak ascending sets. Building on these, it implements and proves termination and correctness for algorithms computing basic sets, characteristic sets, and zero decompositions. In particular, it verifies the well-ordering principle relating a polynomial system to its characteristic set and shows that zero decomposition expresses the original zero set as a union of zero sets of triangular sets away from the zeros of the corresponding initials.

Significance. If the formalization faithfully captures the classical notions, the result is significant: it supplies machine-checked proofs of termination and correctness for the Wu-Ritt method, which underpins much of algebraic geometry and automated geometric theorem proving. The explicit verification of the well-ordering principle and the zero-set decomposition property provides a reliable, certified foundation for polynomial system solving that goes beyond informal arguments.

minor comments (3)

The distinction between standard and weak ascending sets is introduced without an accompanying concrete example or small polynomial system; adding one in the definitions section would clarify the subsequent algorithm statements.
The introduction would benefit from a short paragraph situating the work against prior formalizations of characteristic sets or triangular decompositions in other provers (e.g., Coq or Isabelle).
Notation for pseudo-remainders with respect to a triangular set is used before its precise inductive definition is given; a forward reference or inline reminder would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of our manuscript, which correctly identifies the core contributions of our formalization of the Wu-Ritt method in Lean 4. We appreciate the recommendation to accept the paper.

Circularity Check

0 steps flagged

No circularity: direct formalization of classical Wu-Ritt method

full rationale

The paper defines core notions (initials, pseudo-remainders, triangular sets, ascending sets) directly from classical algebra, then implements algorithms for basic sets, characteristic sets, and zero decompositions while proving termination and correctness inside Lean 4. All load-bearing steps are explicit definitions plus inductive proofs on those definitions; no claim reduces to a fitted parameter, a self-referential equation, or an unverified self-citation. The well-ordering principle and zero-decomposition equivalence are verified against the formalized objects themselves, providing machine-checked evidence independent of the present development.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The formalization rests on standard algebraic definitions of polynomials, pseudo-division, and triangular sets; no free parameters, ad-hoc axioms, or new entities are introduced beyond classical mathematics.

axioms (1)

standard math Standard properties of polynomial rings, pseudo-division, and well-ordering on monomials
Invoked throughout the definitions of initials, remainders, ascending sets, and the well-ordering principle.

pith-pipeline@v0.9.0 · 5457 in / 1249 out tokens · 89187 ms · 2026-05-10T08:40:09.063801+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 3 canonical work pages · 1 internal anchor

[1]

In: Jouannaud, J.P., Shao, Z

G \'e nevaux, J.D., Narboux, J., Schreck, P.: Formalization of Wu 's simple method in Coq . In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs. pp. 71--86. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)

2011
[2]

Guo, J., Shen, H., Liu, J., Zhi, L.: Formalizing Gr\"obner basis theory in Lean (2026), https://arxiv.org/abs/2602.12772

work page internal anchor Pith review Pith/arXiv arXiv 2026
[3]

de Moura and S

de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. p. 625–635. Springer-Verlag, Berlin, Heidelberg (2021). doi:10.1007/978-3-030-79876-5_37, https://doi.org/10.1007/978-3-030-79876-5_37

work page doi:10.1007/978-3-030-79876-5_37 2021
[4]

LogiCal Project (2010)

The Coq Development Team : The Coq Proof Assistant Reference Manual, Version 8.3. LogiCal Project (2010)

2010
[5]

Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho

The mathlib Community : The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 367–381. CPP 2020, Association for Computing Machinery, New York, NY, USA (2020). doi:10.1145/3372885.3373824, https://doi.org/10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824 2020
[6]

Journal of automated Reasoning 2(3), 221--252 (1986)

Wu, W.T.: Basic principles of mechanical theorem proving in elementary geometries. Journal of automated Reasoning 2(3), 221--252 (1986)

1986
[7]

Kluwer Academic Publishers (2001)

Wu, W.T.: Mathematics mechanization: mechanical geometry theorem-proving, mechanical geometry problem-solving, and polynomial equations-solving. Kluwer Academic Publishers (2001)

2001
[8]

, " * write output.state after.block = add.period write

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...
[9]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...