Catalog

Every one of these is still open.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.