{"id":"palomar/PALOMAR-2026-10-01-000010","url":"https://github.com/zblore/gleason-finite-lean/tree/3a9449ce0e3e9f9355f15827ce5d99a4460efa0c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000010-v1.json","repo":"https://github.com/zblore/gleason-finite-lean","tags":["math-ph","quant-ph","msc:81P10","msc:81P16","msc:46C05","msc:46N50","quantum-foundations","gleason-theorem","frame-functions","lean"],"score":0,"title":"gleason-finite-lean","trust":"high","domain":"math-ph","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"math-ph","summary":"A machine-checked proof of Gleason's theorem in finite dimensions. On a complex Hilbert space of dimension at least 3, every frame function on the orthogonal projections has the form P ↦ Re Tr(ρP) for exactly one density operator ρ. The statement is Kim Morrison's lean-eval problem gleason_theorem_finite, unchanged. The proof follows Cooke, Keane and Moran's elementary proof of Gleason's core lemma for matrices on ℂᴺ, then moves the result to operators by taking matrices in an orthonormal basis.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"Measures on the closed subspaces of a Hilbert space","identifier":"https://doi.org/10.1512/iumj.1957.6.56050","relationship":"formalizes"},{"title":"An elementary proof of Gleason's theorem","identifier":"https://doi.org/10.1017/S0305004100063313","relationship":"formalizes"}]}