[kronicum2025]

I'm leaning a lot into AI + lean. It's a fantastic tool to find new proofs. The extremly rigid nature of lean means you can really check programs for correctness. So that part of AI is solved. The only thing that remains is generating proofs, and that is where there's nothing in AI space right now. As soon as we do get something, our mathematical knowledge is going to explode.

[vonnik]

What kind of math do you do, and what would “generating proofs” look like do you think?

[vonnik]

i don't know why this was down-voted... i'm genuinely interested in the answers. feel free to dm me.