nperez19
Joined 5 months ago
Karma
8
Submissions
4
Member since
May 22
Recent submissions
Comment · 24 days ago
There's an entire paper claiming that many of these AI-generated Lean proofs are formulated incorrectly / mistranslated: https://arxiv.org/abs/2610.08144
Comment · 2 months ago
This is the actual link to the academic paper (https://arxiv.org/pdf/2204.00764)
Comment · 2 months ago
Love the pendantic mode setting on the website
Comment · 5 months ago
At the moment Zero doesn't look compelling enough to use it over other more familiar languages. They need benchmarks to show that it has a substantial advantage over other languages (10x more performant, 10x less security vulnerabilities, 10x more maintainable, etc) because at the moment to main sell is that it slightly reduces token consumption and makes the error output slightly nicer.