Appolonian circle packings

Stream: new members

[Lars Ericson]

Possible Lean use case: https://www.quantamagazine.org/two-students-unravel-a-widely-believed-math-conjecture-20230810/

[Joseph Myers]

Are you proposing a project to formalize this proof? (I think "theorems featured in Quanta" would be one worthwhile source - among many other sources - of ideas for a thousand-theorems list of formalization challenges.)