Jacobian Formal

Problem

Investigate formal components of the Jacobian Conjecture.

Approach

Lean 4 and Mathlib infrastructure for formal derivatives, Jacobian matrices, and related algebraic obligations.

Verification and limits

The README calls this partially verified infrastructure. This page does not claim a proof of the general Jacobian Conjecture.

This project summary reviews public documentation. It does not substitute for the project's build, tests, proof audit, or independent evaluation.

License

Not specified in root. The actual project terms govern use.