Distinct distances in general position: an explicit improvement of the bound n/3

Let P be a set of n points in the plane with no three points collinear and no four points concyclic. Every circle centred at a point of P holds at most three other points of P, so P determines at least (n − 1)/3 distinct distances. We prove that every such set with n ≥ 10⁴ points determines more than (1/3 + 1/40)n distinct distances. The proof first shows that a set with few distances lies in a thin annulus around its centre of mass. It then derives linear inequalities that the distribution of the pairwise distances must satisfy, and closes with an exact rational Farkas certificate over 60 cases: nonnegative rational weights such that the weighted sum of the inequalities is false for every possible distance profile. An independent exact verifier (Python standard library only) checks the certificate. The complete proof, with the certificate, is formalized in Lean 4 with Mathlib; the 60 certificate cases are checked by decide +kernel, and the final theorem depends only on the axioms propext, Classical.choice and Quot.sound. The paper is written for readers with an undergraduate background and has 11 figures. Use of AI: AI agents, among them ChatGPT 6.0 Astra (OpenAI) and Claude (Anthropic), developed the arguments, the certificate and its verifier, wrote the Lean definitions and proofs, and wrote the text with the author, under the direction of the author. The results have not been peer reviewed. This record contains the paper (PDF and LaTeX source, with the figures and the programs that draw them), the certificate, the verifier, and the Lean 4 formalization. The paper text and figures are licensed under CC BY 4.0 (paper/LICENSE); the verifier, the certificate, the Lean sources and the figure programs are licensed under the Apache License 2.0 (LICENSE).