News for hackers. Stuff that matters.

MJGrzymek

I was just thinking about how it's an underrated open problem which pairs of (number of variables, degree) are undecidable for MRDP.

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.

I get net::ERR_CERT_COMMON_NAME_INVALID on everwilds.io (chrome android)
Re:DeepSeek-Prover-V2 on Wednesday April 30, 2025 @09:25PM (#43852732)
That's surprising to learn.

I'm surprised those even use actual lean code instead of like raw type theory.

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.
sticking to dfs, there is still a difference between pre-order/in-order/post-order
Re:Are We AI Math Yet? on Friday April 25, 2025 @10:37PM (#43800432)
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.

Re:Four Years of Jai on Friday April 18, 2025 @12:30PM (#43729593)
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.

Re:OpenAI in Talks to Buy Windsurf for About $3B on Wednesday April 16, 2025 @03:14PM (#43709245)
I don't get it, surely they can build it for less than $3B, and why would they need the Windsurf brand?
Re:JSX over the Wire on Wednesday April 16, 2025 @08:33AM (#43704601)
Reading the linked article https://htmx.org/essays/how-did-rest-come-to-mean-the-opposi... , does this mean Next.js is the real REST?

I still can't get over how the "API" in "REST API" apparently originally meant "a website".

I'm a potential user in the wiktionary frontend market cause I'm addicted to checking pronunciations but it seems the support is not great, for example searching "dog" there is no IPA.
You can also see my post on reddit where I answer some questions https://www.reddit.com/r/ProgrammingLanguages/comments/1jfxj...

Show HN: I made PeanoScript, an educational TypeScript-like theorem prover

https://peanoscript.mjgrzymek.com/tutorial

Hi HN, I made this with the idea that many people are somewhat familiar with TypeScript and first-order logic, so combining them could be a nice introduction to automated theorem proving. My CS freshman logic class woefully lacked an interactive code environmentIt's completely web-based so you can go ahead and try the interactive tutorial https://peanoscript.mjgrzymek.com/tutorial . Everything...

( Read More... | 1 comment | 2 points | on HN )
Isn't that trivial in a sense? Encrypt with layer 1, then use that encrypted channel to send layer 2 (and so on). Not sure about the performance.

Signal has a post about using pre and post-quantum together: https://signal.org/blog/pqxdh/

> The essence of our protocol upgrade from X3DH to PQXDH is to compute a shared secret, data known only to the parties involved in a private communication session, using both the elliptic curve key agreement protocol X25519 and the post-quantum key encapsulation mechanism CRYSTALS-Kyber. We then combine these two shared secrets together so that any attacker must break both X25519 and CRYSTALS-Kyber to compute the same shared secret.

Re:Vine: A programming language based on Interaction Nets on Saturday February 22, 2025 @08:52PM (#43145472)
This is something I never got through my annual rechecking of the interaction nets wiki page, cause isn't the lambda calculus also fundamentally parallel? Are nets even more?
Re:Parsing JSON in 500 lines of Rust on Wednesday February 19, 2025 @09:10AM (#43102330)
I got log in page on first click but it went away after closing it and opening again.