{"id":"palomar/PALOMAR-2026-10-04-000005","url":"https://github.com/vltanh/lean4-adr11/tree/2db7f81359758bc49f52bc13c51f2640f8f2a7fd","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000005-v1.json","repo":"https://github.com/vltanh/lean4-adr11","tags":["q-bio.PE","math.PR","msc:92D15","msc:60J90","msc:60J27","msc:05C05","msc:62P10","phylogenetics","coalescent","species-trees"],"score":0,"title":"Identifying the rooted species tree from unrooted gene trees under the coalescent","trust":"high","domain":"q-bio.PE","source":"palomar","authors":["The-Anh Vu-Le"],"reviews":0,"subject":"q-bio.PE","summary":"A formalization of E. S. Allman, J. H. Degnan and J. A. Rhodes, \"Identifying the rooted species tree from the distribution of unrooted gene trees under the coalescent\", J. Math. Biol. 62 (2011) 833-862. The multispecies coalescent is defined from Kingman's coalescent on forests of gene lineages (its generator, the matrix exponential, and a recursion over the species tree). Proved: the distribution of unrooted topological gene trees, with one lineage sampled per taxon, determines the rooted species tree and its internal branch lengths when there are at least five taxa (Theorem 9); on four…","category":"research","comments":0,"disputed":false,"division":"q-bio","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"Identifying the rooted species tree from the distribution of unrooted gene trees under the coalescent","identifier":"arXiv:0912.4472v2","relationship":"formalizes"}]}