{"id":"palomar/PALOMAR-2026-09-13-000003","url":"https://github.com/pro20541/dimitrov-conjectures-lean/tree/95809b59deefd8dfad81e398250aedd7e1aea3b3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-13-000003-v1.json","repo":"https://github.com/pro20541/dimitrov-conjectures-lean","tags":["math.NT","msc:11A25","msc:26D15","number-theory","lean","arithmetic-functions"],"score":0,"title":"Lean proofs of Dimitrov's Conjectures 1 and 3","trust":"high","domain":"math.NT","source":"palomar","authors":["Michael Mazur"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization proving Dimitrov's Conjectures 1 and 3 for every natural k >= 1 and n >= 2. The results concern inequalities involving Euler's totient, Dedekind's psi function, and the sum-of-divisors function. The source paper proves the k = 1 instances and discusses k = 2, 3; this development covers the full stated range, including k >= 4, and additionally proves for each inequality that equality holds exactly when n is prime. By supplying the full parameter range and sharp equality cases beyond those treated in the source, the project is relevant to researchers in elementary and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-13","reactions":{},"formalized":true,"formalizes":[{"title":"Lower bounds on expressions depending on the functions phi(n), psi(n) and sigma(n), III","identifier":"arXiv:2606.12484v1","relationship":"formalizes"}]}