They were looking at 16 variables, degree of about 10 in each one. That search space is simply too big for a plain bruteforce. So they did some sort of filtering to reduce the search space to a pool containing "possible counterexamples".
There was also a paper giving a lower bound of about 100 for possible counterexamples in that particular framework. Later raised to 108 in https://arxiv.org/abs/2204.14178
I don't remember the details very well since this was back in 2015 and wasn't really involved in the research. Consider this to be some sort of telephone game between what I heard in 2015 and what I remember today.
A little over 10 years ago I remember meeting a postdoc who believed he had something close to a counterexample to the Jacobian Conjecture. He and another person was bruteforcing polynomials in about 16 variables, something like 80 - 700 terms each, using binary trees for mapping coefficients.
They were guessing, at the time, that the lower bound of a counterexample (P, Q) for max(deg(P), deg(Q)) would go up to 200.
To think that Claude Fable was able to find a counterexample in degree 7 is insane to me. We are truly in a new era.
Ironically, on the Japanese net, you'll find people complain about the "low range" of EVs compared to hybrids, meanwhile most people in the car-centric areas of Japan don't travel (let alone drive) outside of their own prefecture.
One complaint that I do think is valid is that many people don't live in a house with their own garage and 240V power line. i.e. dedicated home charging is impossible for many people.
Recently had to touch a Python project at work. Just setting up the editor needed me to use 2-3 tools out of: pyright, basedpyright, ruff, ty, mypy, and possibly other tools I'm forgetting that kind of do the same thing but throw errors in different parts of the codebase.
Also, for some reason Optional[T] became deprecated, just as the ecosystem finally embraced types ~3 years ago.
In fact, one my company's greenfield projects decided to use TypeScript instead of Python for the [surprisingly] more consistent tooling, and the fact that the big LLM providers all have official TypeScript SDKs anyway. Also, for agentic coding, LLMs don't seem noticeably worse at TypeScript than Python.
My experience can be summarized as:
- for some reason we need 2-3 static analysis tools just for typechecking
- no tool understands each other's comment directives
- each tool reports a different error in your codebase
- even big libraries (e.g. matplotlib) make half their functions return Any
- you'll be tempted to silence the "partially unknown type" warnings, and you'll have to do it for each tool that's running.
It doesn't mean "we believe reality works this way". It means "at extremely small scale, probabilistic models from QM best predict the behavior of electrons".
Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it.
Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago.
I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
Many organizations, surprisingly, still do things like using Kubernetes with TLS terminated at the ingress. In that case, you just need the splitter in the same network as the nodes hosting the ingress controller. Or inspect the unencrypted traffic within the cluster.
It takes a non-trivial amount of work to set up a service mesh (and mutual TLS between services), so many k8s clusters end up with unencrypted traffic inside the cluster network.
1. TypeScript doesn't aim to have a sound type system. i.e. there may be things the type system accepts that are actually unsafe.
2. this is more of an issue with mutation. If those properties were marked `readonly`, then the assignment of y.a wouldn't work at all. You can also encapsulate mutation behind functions with your intended types.
I tend to write TypeScript in a "functional" or "immutable" way, and in this case, most soundness issues come from things like array index access, which can't really be solved without dependent types anyway.
With that said, TypeScript still gets one quite far *despite* soundness not being a goal of the type system. The problem is that writing imperative, mutable code will make you go through (intentionally!) unsound covariance of types. Similar issues exist for code with side effects, since TypeScript has no way to encode effects in the type system. This is why some language communities settle on ideas like "functional core, imperative shell", where the ultimate goal is absolute minimum amount of code involved in side effects and mutation, while everything else is designed to be easy to test (and, ideally, expressible with a sound subset of your type system).
There is a mobile game I know of that had an outage as a result of a GCP service outage. That is the only time I've noticed GCP outages.
With that said, I would not say few companies rely on GCP. Search for "GCP" in this month's HN hiring thread. There are 23 hits, more than Azure's 21. AWS has 90 hits, which I guess shows its sheer dominance in the startup space. But these figures more or less agree with my intuition of the major clouds being AWS/GCP/Azure.
Pretty much every mountainous region in the mainland of Japan, except for Chiba prefecture, has bears. Most people do not live in the mountains, which is why bear sightings tend to be limited to the areas with (a) significant human population, (b) proximity to mountains.
Since the OP stated they used DeepSeek V4 Flash for generating a lot of the code, I decided to check whether there were any outdated dependencies. In my experience, with Rust projects, if you do not instruct models (even Claude 4.7 Opus) to use `cargo add` instead of manually editing the Cargo.toml, you will almost certainly get out-of-date dependencies added to your project.
Manually checking the dependencies used by this project, I was pleased to see they are all the latest version. That doesn't mean there are no issues lurking in transitive dependencies, of course.
As for getting an LLM to review the code, I think we can get all opinionated very fast. For instance, when I was eyeballing the code, some of the enum methods converting to/from strings made me think "this could've been a single #[derive] with strum." That would make the code in provider.rs a lot more concise, at the cost of importing one crate (with no dependencies!)
Lastly, for fun, I decided to get DeepSeek V4 Pro (with Max thinking) to "audit" the codebase. The output mentioned no obvious signs of hidden telemetry, but it did note that the project sets the panic handler to "abort", which I have strong opinions on... Presumably the OP wanted to avoid linking against libunwind to save a few kilobytes of binary size, but now you have a binary that immediately aborts and doesn't give the user a stacktrace of what just crashed. I would rather have a ~50 KiB larger binary if it means getting useful debug info during a panic. Additionally, if there are async tasks that panic, they can't be recovered to display a generic error message; instead the whole process just aborts.
I noticed borkdude posted this thread *and* he is listed as a contributor for this release.
For the longest time, I recall the opposition to async/await support being twofold:
1. adding support would require deep changes across the CLJS compiler (theller, creator of shadow-cljs, once tried and concluded this)
2. macros from libraries like Promesa provided similar convenience
There were some other arguments brought up at the time (e.g. just use core.async, expression-oriented languages aren't a good fit with async/await, etc.), but they were usually specific to one person rather than something you'd see repeated in forums.
In the Clojurians Slack, borkdude once stated he wasn't convinced it'd be impractical to add support. It seems that he eventually took the time and made it happen. Extremely thankful for that.
MPEG-2 TS is a container. H.264 is a coding specification. They are totally different things.
One can find MPEG-2 TS in surprising places (see: DOCSIS encapsulating Ethernet frames into TS packets).
If I had to guess why MPEG-2 TS, it'd probably be the for the fact it's a well-supported streaming format in both hardware and software. If you tried using QuickTime or MPEG-4 containers, you'd have to rely on hacks like ensuring the moov atom preceeds mdat.
Matroska may be worth considering (especially the subset used by WebM to make it stream-friendly and quicker to seek), but no idea how widespread hardware support is for (de)muxing that.
For what it's worth, Kine (software that k3s uses to replace etcd with SQL databases) implements etcd watches on SQLite through polling[1]. The reason being that SQLite does not offer NOTIFY/LISTEN like MySQL and Postgres do. Ironically, Honkey attempts implementing NOTIFY/LISTEN through polling.
k3s has been running on my home server for about three years now (using the default SQLite backend), and there doesn't seem to be excessive CPU usage despite dozens of watches existing in the simulated etcd. Of course, this doesn't say much about Honker, but it's nonetheless worth pointing out that sometimes the choice of database forces one towards a certain design.
Most of the rail has get around mountainous, uneven terrain subject to earthquakes, strong winds, and heavy rain. California should be able to build rail parallel to the I-5, a long, flat terrain without extreme weather or strong earthquakes. The problem seems to be a political one, not an engineering one. In fact, if the Interstate Highway System did not already exist, I doubt the U.S. today would be able to accept and complete it.
> one long line with a few branches
I currently live in Japan, and that does not really match what I've observed. There are three distinct railway companies in my area (JR, Tokyu, Yokohama Municipal Subway), each with their own dedicated rail, trains, power supply, etc.
The situation is more like "a disjoint union of graphs, where some of the graphs are connected".
At my current job, I sometimes set up a Nix shell with the GitHub CLI, since that let's Claude Code associate a feature branch to a pull request. The LLM can then retrieve PR description, workflow results, review comments, etc.
Also, I believe GitHub Actions cache cannot be bulk deleted outside of the CLI. The first time I [hesitantly] used the gh CLI was to empty GitHub Actions cache. At the time it wasn't possible with the REST API or web interface.
> what do these LLM clichés look like in Japanese?
Besides text reading like a machine translation, the tell-tale signs often involve things like:
- itemized lists (I know, it's ironic that I'm using them here)
- frequent use of conjunctions
- use of demonstratives that feels redundant
- full-width colons, especially in titles
- subheadings that always end in abstract nouns
- bold text, especially at the beginning of a line
The demonstrative bit may be hard to express, but to give you an idea: when communicating in Japanese, words that can be understood from context may be omitted. Explicitly writing out words understood from context can sometimes make a sentence sound redundant.
Before LLMs were widespread, SEO spam in the Japanese net tended to be affiliate sites with predictable, template paragraphs. I get reminded of those sites whenever GPT starts a response with 「結論から言うと、〇〇」, since that's exactly how those affiliate sites wrote back in the day.
The intent is to have a proof of some proposition. The Lean runtime crashing doesn't stop the lean-zip developers from formally modelling zlib and proving certain correctness statements under this model. On the other hand, the Lean kernel having a bug would mean we may discover entire classes of proofs that were just wrong; if those statements were used as corollaries/lemmas/etc. for other proofs, then we'd be in a lot of trouble.
When I see a title transitioning from "Lean said this proof is okay" to "I found a bug in Lean", I'm intuitively going to think the author just found a soundness (or consistency) issue in Lean.
Yeah, the title made me think the author found a bug in the Lean kernel, thus making an invalid proof pass Lean's checks. The article instead uncovers bugs in the Lean runtime and lean-zip, but these bugs are less damning than e.g. the kernel, which must be trusted to be correct, or else you can't trust any proof in Lean.
There was also a paper giving a lower bound of about 100 for possible counterexamples in that particular framework. Later raised to 108 in https://arxiv.org/abs/2204.14178
I don't remember the details very well since this was back in 2015 and wasn't really involved in the research. Consider this to be some sort of telephone game between what I heard in 2015 and what I remember today.