10. Four Exponentials
Status: target stated. No proof of the conjecture.
This is a separate Lean library in the same repository. Hardy is complete. Sharp Five Exponentials is the current priority. Work on Four Exponentials follows a successful Sharp Five proof. The Jacobian Conjecture was a source of motivation, not an additional project.