{"id":"palomar/PALOMAR-2026-09-27-000004","url":"https://github.com/jfairfaxball-348/Petersen-Zero-Forcing/tree/5dd760e79ab33b3fcf2feb93eb37e23509d184ed","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-27-000004-v1.json","repo":"https://github.com/jfairfaxball-348/Petersen-Zero-Forcing","tags":["math.CO","msc:05C50","graph-theory","zero-forcing","lean-formalization","generalized-petersen"],"score":0,"title":"Zero forcing number of the generalized Petersen graphs P(n,3)","trust":"high","domain":"math.CO","source":"palomar","authors":["John Fairfax-Ball"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 proof that the zero-forcing number of the generalized Petersen graph P(n,3) is exactly 8 for every natural number n >= 13. The formalized result is the statement recorded as Conjecture 5 in Arnav Krishnan's July 2026 correction preprint; this repository supplies and kernel-checks a proof of that conjectured statement rather than formalizing a proof already given in the cited preprint.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-27","reactions":{},"formalized":true,"formalizes":[{"title":"A correction to the Zero Forcing Number of the Generalized Petersen Graphs P(n,3)","identifier":"arXiv:2607.19412v1","relationship":"formalizes"}]}