I get net::ERR_CERT_COMMON_NAME_INVALID on everwilds.io (chrome android)
Readit NewsMJGrzymek commented on Show HN: MMORPG prototype inspired by World of Warcraft github.com/nickyvanurk/ev... · Posted by u/nickyvanurk
I wonder if the authors have tried incorporating error feedback from Lean into their models.
Work from 2023 [1] showed general purpose models did better when they were able to incorporate error feedback, humans incorporate error feedback, but none of the SOTA models on minif2f seem to.
That's surprising to learn.
I'm surprised those even use actual lean code instead of like raw type theory.
MJGrzymek commented on Ask HN: Will employers care less about math contests as AI gets better at them? · Posted by u/amichail
They shouldn't - they never wanted people to solve these math problems on the job, they're using the ability to solve them as a proxy for other abilities, which will likely fall to AI later.
MJGrzymek commented on Programming languages should have a tree traversal primitive blog.tylerglaiel.com/p/pr... · Posted by u/azhenley
sticking to dfs, there is still a difference between pre-order/in-order/post-order
The (self-posting) author here.
I follow some math professors, so I linked their relevant stuff, but I was surprised how little quality commentary I could find. Please link if I missed something.
Well, 1) the temporary allocator strategy; and 2) `defer` kinda go against the spirit of this observation.
With (1) you get the benefits of GC with, in many cases, a single line of code. This handles a lot of use cases. Of those it doesn't, `defer` is that "other single line".
I think the issue being raised is the "convenience payoff for the syntax/semantics burden". The payoff for temp-alloc and defer is enormous: you make the memory management explicit so you can easily see-and-reason-about the code; and it's a trivial amount of code.
There feels something deeply wrong with RAII-style langauges.. you're having the burden to reason about implicit behaviour, all the while this behaviour saves you nothing. It's the worst of both worlds: hiddenness and burdensomeness.
Not sure about the implicit behavior. In C++, you can write a lot of code using vector and map that would require manual memory management in C. It's as if the heap wasn't there.
Feels like there is a beneficial property in there.
MJGrzymek commented on OpenAI in Talks to Buy Windsurf for About $3B bloomberg.com/news/articl... · Posted by u/mfiguiere
I don't get it, surely they can build it for less than $3B, and why would they need the Windsurf brand?
Correct me if I'm wrong but I think it's guaranteed to have a finite answer, as a list of the minimal undecidable pairs. You can even throw in maximum absolute value of coefficients, though if you limit all three things that's decidable by being finite.