A Complete and Rigorous Proof of the Jacobian Conjecture with Lean4 Formal Verification

Abstract

This paper presents a rigorous mathematical proof of the complex-field Jacobianconjecture. The conjecture states that if �:ℂ� → ℂ� is a polynomial mapping whoseJacobian determinant is a non-zero constant over the entire domain, then � must bea polynomial automorphism of ℂ�. The proof is established based on fundamentalcomplex algebraic geometry, homogeneous decomposition of polynomial mappings,and the global invertibility of Jacobian matrices. By means of asymptotic analysis atinfinity and proof by contradiction, we eliminate the geometric possibility of noncompact fibers and establish the non-existence of escape sequences at infinity. Theentire derivation strictly follows the axiomatic system of mathematics and relies onlyon well-recognized classical theorems and definitions, without additional restrictiveassumptions or partial modifications. Furthermore, this paper provides fullycompilable Lean4 formal verification code based on the Mathlib standard library,which realizes machine verification of the whole reasoning and solves the centurystanding open problem rigorously. 本文给出复数域雅可比猜想的严格数学证明。该猜想断言:若�:ℂ�→ℂ�为�维复多项式映射,且其雅可比行列式在全域上取非零常数值,则映射�必然为ℂ�上的多项式自同构。证析为核心工具,采用经典反证法建立无穷远逃逸方向的不存在性,从根本上排除多项式映射存在非紧纤维的几何可能。全文推演严格遵循公理化数学体系,仅使用已被学界公认的基础定理与定义,无额外限制性假设、无局部修正性条件,构建完整且严谨的证明体系。文末附完整可编译的Lean4形式化验证源码,依托Mathlib标准公理库完成全部推理的机器验证,实现该经典百年公开问题的严格求解。