maths_math

9 ms·

1. 1.▲
   by maths_math 6d ago

   What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...
2. 2.▲
   by maths_math 6d ago

   > humans don't need to be involved in scientific advances to benefit. I agree with you on this point in isolation, but I think it's missing an enormous amount of context. Humans can absolutely benefit from science they weren&#x
3. 3.▲
   by maths_math 7d ago

   As I've commented elsewhere in this thread - if your goal is really to have people use LLMs to further mathematical understanding for humanity, instead of to brag about "solving" open problems, then why is there an explicit p
4. 4.▲
   by maths_math 7d ago

   Steam engines actually replaced what a horse does with a machine that could do the same job. So far LLMs aren't doing this - they're producing Lean proofs but very little to actually aid in understanding (again so far pretty m
5. 5.▲
   by maths_math 7d ago

   > If the value on the other hand comes from people being extremely good at math, rather than from them solving novel open problems, then we should pay them to do that, which is independent of whether the open problems are solved or not.