Lean repository linked
The Wallace problem and countably compact torsion-free Abelian groups in ZFC
arXiv:2608.17317 · arXiv
Lean formalisations (1)
vo-rodrigues/wallace-problem-palomar at 1ab2fb7ed1fb
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.