{"id":"palomar/PALOMAR-2026-09-30-000015","url":"https://github.com/mbucic4/Nearly-spanning-Lovasz/tree/7f2728d07ce648ed74cae08bbfa7084b9ec13f4b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000015-v1.json","repo":"https://github.com/mbucic4/Nearly-spanning-Lovasz","tags":["math.CO","msc:05C45","msc:05C38","lean","graph-theory","vertex-transitive","lovasz-conjecture"],"score":0,"title":"Near-linear cycles in connected vertex-transitive graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Matija Bucic"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of the near-linear cycle theorem in \"Lovász conjecture holds asymptotically\". For every positive ε, sufficiently large connected finite vertex-transitive graphs contain a simple cycle with at least n^(1−ε) edges. The development includes a weaker-constant Bondy–Locke path-to-cycle comparison and the finite approximate-group and expansion arguments used in the path proofs.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Lovász conjecture holds asymptotically","identifier":"","relationship":"formalizes"}]}