MJGrzymek
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'm surprised those even use actual lean code instead of like raw type theory.
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.
Are We AI Math Yet?
Feels like there is a beneficial property in there.
I still can't get over how the "API" in "REST API" apparently originally meant "a website".
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...
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.