{"id":"palomar/PALOMAR-2026-09-25-000002","url":"https://github.com/sascha2718/qi-trees-and-matching-lean/tree/35e78969d036b4f663fc9a96d8c22750834a6ac4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000002-v2.json","repo":"https://github.com/sascha2718/qi-trees-and-matching-lean","tags":["math.PR","math.GR","math.MG","msc:60J80","msc:51F30","msc:30L10","msc:28A80","msc:60K35","msc:68V20","galton-watson-trees"],"score":0,"title":"The quasi-isometry classes of Galton–Watson trees: Lean formalisation","trust":"high","domain":"math.PR","source":"palomar","authors":["Jayadev S. Athreya","Sascha Troscheit"],"reviews":0,"subject":"math.PR","summary":"Lean 4 formalisation of the automorphism-matching theorems and the quasi-isometry classification of Galton–Watson trees from the paper \"The quasi-isometry classes of Galton–Watson trees\" by Jayadev S. Athreya and Sascha Troscheit (arXiv:2609.23882). The audited statements are: the i.i.d. matching theorem on the binary tree (Theorem 5.1), the general Markov matching theorem for typed label processes on the binary tree, in its finite-type and zero-compatible forms (Theorem 6.1), the complete classification, up to quasi-isometry, of Galton–Watson trees with finitely supported offspring law…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"The quasi-isometry classes of Galton–Watson trees","identifier":"arXiv:2609.23882","relationship":"formalizes"}]}