Eclecta | today's edition

• The test: implement the full 835-page SQLite manual in Rust with source code, test suites, the SQLite binary, and internet access withheld; graded against sqllogictest (millions of queries), which the swarm was never told existed. Cursor manually reviewed runs for cheating.
• Architecture is two roles over a recursive task tree: planner agents (frontier models) decompose and delegate and never implement; worker agents (cheap/fast models) execute leaves and never plan. Cursor attributes the gains mainly to context efficiency, not parallelism, since a planner's context never fills with low-level detail.
• New vs old harness on Grok 4.5: new hit 80% in four hours; old was paused before hour two after 68,000 commits (~70x the new pace) and 70,000+ merge conflicts still accelerating, vs under 1,000 conflicts for the new run. Old run sprawled to 54 crates (three separate SQL packages); new settled on nine.

Cursor describes a planner/worker agent swarm that decomposes a large task into a recursive tree: frontier-model planners split goals and make design decisions, while cheaper, faster worker models execute the leaves. To benchmark it, the team had the swarm reimplement the 835-page SQLite manual in Rust from documentation alone, with source, tests, binary, and internet withheld, grading against the sqllogictest suite. The new harness beat an earlier swarm in every model configuration: on Grok 4.5 it reached 80% in four hours where the old swarm spiraled into 70,000+ merge conflicts and was paused before hour two, and it did so with far less code (e.g., 4,645 vs 19,013 lines in one mix). Costs varied from $1,339 for an Opus-planner/Composer-worker hybrid to $10,565 for GPT-5.5 alone, because workers carry most tokens but planner tokens are pricier. Supporting infrastructure includes a from-scratch version control system handling ~1,000 commits/second and coordination mechanisms for duplicate work, planner conflicts, merge collisions, and 'megafiles.' All figures are self-reported by Cursor; the model versions are unreleased-tier names, and the public minisqlite repo has not been deeply audited.

• Reframes open-weights economics: 'free' refers only to R&D (a fixed cost); COGS scales with revenue. Example: $0.50 inference cost per $1 of revenue means $50M COGS at $100M revenue, $50K at $100K.
• Price comparison from the article: Kimi K3 at $3/M input and $15/M output tokens vs Sol at $5/M input and $30/M output, but Kimi reportedly burns far more reasoning tokens, which the author says erases the nominal advantage.
• Central claim: tokens are not fungible across models, so tokens are not the commodity; intelligence (the correct answer) is. Cost of intelligence is driven by model footprint, MoE inference efficiency, KV-cache/memory efficiency, serving tricks (batching, prefix caching), and token efficiency. Author disputes Jensen Huang's 'token factory' framing for the reasoning era.

Ben Thompson (Stratechery) argues the panic over near-frontier Chinese open-weight models like Moonshot's Kimi K3 and Alibaba's Qwen3.8 Max is economically overblown. His core distinction: open weights are 'free' only in R&D (a fixed cost), while inference is real COGS that scales with revenue, so serving models is not free. He contends tokens are not a commodity because different models need different numbers of reasoning tokens to reach the same answer; the fungible good is intelligence, whose cost depends on model footprint, MoE efficiency, memory/KV-cache use, serving optimizations, and token efficiency. Applying commodity-market mechanics, he claims Chinese models only look cheaper because a compute shortage lets Anthropic and OpenAI price far above marginal cost, and that frontier labs, who serve at the lowest cost and improve fastest, are best positioned even in commoditizing lower tiers. On policy, he says China is commoditizing its complements (open models feeding its robotics/physical-world lead), argues US open-weight makers are handicapped by frontier labs' anti-distillation terms of service, and proposes a law making training data fair use and banning distillation bans. He names cybersecurity as the one genuine concern, citing a Hugging Face breach report where US frontier-model guardrails locked out defenders, forcing reliance on China's GLM 5.2, and calls for loosening US restrictions so defenders can use the best models.

• git has two distinct terminators: `--` separates revisions from pathspecs (so `git log main -- README.md` reads as commits on main touching that file), leaving the revision slot with no terminator; `--end-of-options`, added in git 2.24.0 (Nov 2019), fills that gap. The safe invocation for an untrusted revision is `git log --end-of-options "$rev" -- "$path"`, with both markers doing separate jobs.
• Subcommand support was staggered: rev-parse only got the flag in 2.30.0 (its own hand-rolled parser), and checkout/reset rejected it until 2.43.1 (Feb 2024) because they parse `--` themselves and left `--end-of-options` in the argv where their parsers choked.
• CWE-88 argument injection needs no shell: the wrapper builds a clean argv and calls exec directly, but git parses a dash-leading argument as an option such as `--upload-pack=<cmd>`, `-c core.sshCommand=<cmd>`; hg has `--config=alias...=!<shell>`, ssh has `-oProxyCommand=<cmd>`. CVE-2019-13139 hit `docker build` this way via a git URL `#ref:dir` fragment.

The article audits adoption of git's `--end-of-options` flag, which exists because git had already repurposed `--` to separate revisions from pathspecs, leaving untrusted revision strings that start with a dash to be parsed as options. This enables CWE-88 argument injection, a shell-free attack where a clean argv reaches git and a dash-leading argument becomes a dangerous option like `--upload-pack=<cmd>` or ssh's `-oProxyCommand`; the author cites CVE-2019-13139 in docker build and a four-VCS coordinated disclosure in Aug 2017. Support for the flag rolled out unevenly (2.24.0 in 2019, rev-parse in 2.30.0, checkout/reset only in 2.43.1), which complicates adoption for tools supporting older git. Of 19 package managers surveyed, 17 fork the git binary and only Go's cmd/go uses `--end-of-options` (added Jan 2026 for CVE-2025-68119); most others rely on `--` or leading-dash checks added reactively as CVE patches, and several tools maintain minimum-git floors below 2.24.0. Alternatives like libgit2, gitoxide, go-git, JGit and dulwich avoid the argv boundary entirely but must track every upstream checkout-safety fix themselves. The author closes by filing a Homebrew PR raising its git floor to 2.30.0 and adding the flag to clone, remote set-url, ls-remote and rev-parse calls.

• MoE model: 119B total, 6B active parameters, Apache-2.0, weights on Hugging Face plus a free API endpoint (leanstral-1-5); trained via mid-training, SFT, then RL with CISPO across a multiturn prove/disprove environment and a filesystem code-agent environment verified by a fork of SafeVerify.
• Self-reported benchmarks: 100% on miniF2F validation and test; 587/672 PutnamBench; SOTA 87% FATE-H and 34% FATE-X; FLTEval pass@8 up from 31.9 to 43.2, beating Claude Opus 4.6's 39.6 at one-seventh the cost. All figures are vendor-reported without independent verification.
• Cost claim: ~$4 per PutnamBench problem, edging Seed-Prover 1.5 (high) by 7 problems at an estimated $300+ per problem (10 H20-days budget); Aleph Prover cited at $54-68 per problem. Higher-ranked provers use natural-language proof guidance or run at far higher cost.

Mistral released Leanstral 1.5, an Apache-2.0 licensed MoE model (119B total, 6B active) for formal proof engineering in Lean 4, with open weights on Hugging Face and a free API. The company reports it saturates miniF2F (100% on validation and test), solves 587 of 672 PutnamBench problems, and reaches state-of-the-art on the abstract-algebra benchmarks FATE-H (87%) and FATE-X (34%), while claiming a large cost advantage of about $4 per PutnamBench problem versus an estimated $300+ for Seed-Prover 1.5 high. Training used mid-training, supervised fine-tuning, and RL with CISPO across a multiturn prove/disprove environment and a filesystem code-agent environment. Mistral highlights monotone test-time scaling (44 to 587 PutnamBench problems as token budget rises from 50k to 4M) and a long AVL-tree proof spanning 2.7M tokens and 22 compactions. A bug-discovery pipeline combining Aeneas Rust-to-Lean translation with Leanstral flagged 47 violated properties across 57 repositories, 11 genuine bugs and 5 previously unreported, including a U64 overflow in zigzag decoding. All benchmark, cost, and bug-count figures are self-reported and lack independent verification or detailed methodology.

• Soteria Rust is an OCaml symbolic-execution tool that checks Rust programs against Tree Borrows, tracking every reference to a memory location as a tree of five-state nodes; each read/write updates node states, and reaching the fault state signals UB.
• The slowdown came from unoptimized MIR: the tool cannot enable compiler optimizations (inlining, dead-code elimination) because they can erase the UB it hunts, so Range::next reborrows persist. Each Iterator::next call adds 9 nodes and ~10 accesses per iteration, giving 9N+10 nodes and 10N+12 accesses (9,010 nodes, 10,012 accesses at N=1000), roughly 45N-squared node accesses.
• Soundness argument for dropping nodes: UB is only reachable via a local access, a finished loop iteration's branch has no live references, protected nodes (on function entry) are kept alive by the interpreter, children are always at least as close to UB as parents, and pre-branch state references prevent cross-branch collection in symbolic execution.

Soteria Rust, an OCaml-based symbolic execution tool that verifies Rust against the Tree Borrows aliasing model, hit quadratic runtime on a simple increment loop because unoptimized MIR generates repeated reborrows (from Iterator::next desugaring) that grow the per-location reference tree by about 9 nodes and 10 accesses per iteration. At N=1000 the tree reached 9,010 nodes and 10,012 accesses, with 87% of the 3.02s runtime inside Tree Borrows. The fix, roughly 40 lines, holds tree nodes weakly using OCaml's Weak sets and Ephemeron and lets OCaml's garbage collector reclaim nodes from finished iterations, justified because UB is only reachable via local accesses on live references. Because OCaml's GC runs too rarely under low allocation, the authors force major collections when the tree exceeds a threshold T (best at 256) with a 2T backoff when nothing is freed. This restored linear time with up to a claimed 10.6x speedup, and cut a scaled Tokio init benchmark from 14.8s to 1.7s, though some benchmarks slowed due to weak-reference overhead. The authors frame this as reusing the host language's GC, contrasting with Miri, which must implement tree GC manually because its host language is Rust.

• Per Risky Business sources, the hacker logged into Romania's ANCPI cadastre agency with valid credentials, mapped internal systems, then wiped systems and backups after failing to extort the agency; data deletion began July 14, and stolen data (employee credentials, internal documents, network details) went up for sale on a hacking forum a day later.
• The agency appears to have kept an offline backup that survived the wipe; officials restored the website and announced they are rebuilding the entire network from scratch. Notaries could not record transactions and citizens could not obtain proof of ownership while apps, sites, and email were down.
• The attacker posts as ByteToBreach; KELA's December profile placed them in Algeria and, after this hack, updated the post to name Zakaria Mahdjoub of Oran, Algeria. Same actor is tied to a breach of Sweden's e-government portal this year.

A hacker breached Romania's National Agency for Cadastre and Real Estate Advertising (ANCPI) using valid credentials, mapped internal systems, and wiped both systems and backups after a failed extortion attempt, according to Risky Business sources. The wipe, which began July 14, took the country's land registry offline for a week, stalling property transactions and blocking citizens from obtaining ownership records; stolen employee credentials, internal documents, and network details were listed for sale on a hacking forum the next day. An offline backup appears to have survived, and the agency is rebuilding its network from scratch. The account behind the leak, ByteToBreach, was profiled by KELA and named as Zakaria Mahdjoub of Oran, Algeria, and is also linked to a breach of Sweden's e-government portal this year. Romania is at least the sixth country in three years to have its land registry hacked. The same Risky Business bulletin separately reports that Hugging Face was breached by an autonomous AI agent exploiting its data-processing pipeline, and that Hugging Face's own model guardrails blocked using a frontier model for incident response.

• Nikkei estimates off-balance-sheet debt across five US tech giants at $1.65tn, up roughly eightfold in about four years; the figure now exceeds these companies' reported on-balance-sheet debt.
• Meta alone carries about $420bn in off-balance-sheet debt, nearly triple its transparent debt, per the study.
• The mechanisms cited are data center leases and GPU supply contracts, arrangements that create liabilities without appearing as conventional borrowing.

A Nikkei study estimates that off-balance-sheet, or "hidden," debt across five US tech giants has reached about $1.65tn, up roughly eightfold in four years as AI investment surged. The study says this hidden debt now exceeds the companies' transparent, on-balance-sheet debt, complicating investors' ability to gauge risk. The liabilities stem from arrangements such as data center leases and GPU supply contracts rather than conventional borrowing. Meta is highlighted with roughly $420bn in off-balance-sheet debt, nearly triple its reported debt. Meta and Oracle are named among the five firms; the excerpt does not list the others or the estimate's methodology. The figures are Nikkei's own estimates rather than audited disclosures.

• An AWS user reported an estimated bill of $1.7 billion for the current month against normal monthly spend under $5.
• The report is a Hacker News post pointing to the AWS Health status page (health.aws.amazon.com/health/status), a Reddit r/aws thread, and an open AWS support ticket.
• Scale is inferred from community activity, not an AWS statement: the HN post hit 1,064 points and 646 comments, and the Reddit thread corroborates other affected accounts.

A Hacker News thread surfaced reports that AWS's estimated billing display showed grossly inflated figures, including one account with normal spend under $5 that displayed an estimated $1.7 billion charge for the month. The affected user opened an urgent AWS support ticket and pointed to the AWS Health status page, with a Reddit r/aws thread suggesting other accounts saw similar anomalies. Community engagement was heavy (1,064 HN points, 646 comments), which is the basis for calling the issue widespread rather than an isolated account glitch. Users describe it as an estimation or display error, not actual charges levied, but the source provides no AWS confirmation of the cause, scope, or whether real invoices are affected. Root cause, timeline, and resolution are absent from the available text.

• Timeline (as reported by Kevin Buzzard): ChatGPT disproved Erdős' Unit Distance conjecture on 20 May 2026 using a Golod-Shafarevich construction; Logical Intelligence (cofounded by Yann LeCun, CSO Fields Medallist Mike Freedman) autoformalized the paper's key implication in Lean within a week; OpenAI's Boris Alexeev used a new model 'Sol' to formalize it from axioms, including hard global class field theory results the author had thought a fantasy to formalize in 2025.
• Scale claim: Sol generated 1.2 million lines of Lean in three weeks; for comparison Lean's mathlib library is 2.3M lines built over nine years. Buzzard ran all AI-generated code in a sandbox because Lean is a full programming language and can execute arbitrary commands.
• Grothendieck's ~60-year question (is every finite free group scheme of order n killed by n?) was disproved with a group scheme of order 4 not killed by 4; Akhil Mathew got a 12-page pdf from Sol, Claude 'Fable' autoformalized it to a 1076-line Lean file in four hours, and Buzzard verified statement and proof in under five minutes before it went to a mathlib PR.

Lean maintainer and mathematician Kevin Buzzard gives a firsthand account of a roughly two-month stretch in mid-2026 in which large language models produced counterexamples to several open mathematical conjectures and then formalized them in the Lean proof assistant. He reports ChatGPT disproving Erdős' Unit Distance conjecture, OpenAI's 'Sol' model generating 1.2 million lines of Lean (versus mathlib's 2.3M built over nine years) to prove it from axioms, a counterexample to a ~60-year Grothendieck question about group schemes of order n, and a claimed counterexample to the century-old Jacobian Conjecture. The formalization angle is central: because DeepMind's Formal Conjectures repo and mathlib encode human-agreed statements, checking AI-generated proofs reduces to compiling code, which Buzzard did in minutes inside a sandbox given that Lean can run arbitrary commands. He notes intense vendor activity (Logical Intelligence, Logos Research, Harmonic, Axiom AI, Moonshot AI, Anthropic's Fable, OpenAI's Sol) and PhD students paying $200/month for access. Buzzard argues large AI-generated mathematical developments are now inevitable, while stressing the open work is for humans to understand why these counterexamples exist. The results are self-reported by named mathematicians and not independently peer-reviewed within the post.

• Team: Simons Foundation Flatiron Institute CCQ (Joseph Tindall, first author; Miles Stoudenmire) with Boston University collaborators, published in Science 2026 (vol 392, p868, DOI 10.1126/science.adx2728).
• Target: dynamics of hundreds of interacting qubits on square, cubic, and diamond lattices, the same class of problem King et al. (many D-Wave authors) argued in a March 2025 Science paper could not be matched classically (DOI 10.1126/science.ado6285).
• Method: tensor networks compress the exponentially large wave function (Tindall's analogy: a zip file of interconnected small number tables), run via CCQ's ITensor library; 3D dynamics modeled with a 3D tensor network the authors call an untrodden frontier and a software-engineering challenge.

Researchers at the Simons Foundation's Flatiron Institute (CCQ) and Boston University report in Science (2026) that they simulated the dynamics of hundreds of entangled qubits on square, cubic, and diamond lattices using tensor networks, with some calculations run on a personal laptop. The problem was chosen deliberately because a March 2025 Science paper (King et al., largely D-Wave authors) had used a quantum computer for this class of dynamics and argued classical machines could not match it. The CCQ team compressed the exponentially large wave function with tensor networks via their ITensor library, and used belief propagation, a cheaper if more approximate 1980s algorithm recently adapted to quantum systems, to reach 3D problems that older exact methods could not start. They say results matched theoretical predictions, checked out on smaller solvable instances, and agreed with the prior quantum-computer results without quantum hardware. The authors frame classical and quantum simulation as synergistic rather than purely competitive, and name electron-hopping systems relevant to real materials as their harder next goal. All accuracy claims are self-reported.

• Baseline chain: Eytzinger layout is ~4x faster than std binary search once data exceeds L3, because it can prefetch 4 cache lines ahead; the S+ tree adds cache-line-dense nodes on top for the claimed 40x. All numbers are self-benchmarked on an i7-10750H pinned to 2.6GHz (32KiB L1, 256KiB L2, 12MiB L3), AVX2 only, no AVX-512, hyper-threading off.
• Node = 16 u32 values = 64 bytes = one cache line, giving branching factor 17; using S+ (values duplicated into internal nodes, every query terminates at the same leaf depth) is what makes batching clean, since every query in a batch takes the same number of steps.
• Batching is the main throughput win: it saturates around 12 in-flight reads, matching the CPU's 12 line fill buffers, cutting amortized RAM wait from ~80ns latency to ~8ns; 1->2 gives sub-linear gain because out-of-order execution already overlaps ~2 queries. Author ships batch size 128 for cleaner plots and slightly lower per-batch overhead.

A detailed engineering writeup that implements and optimizes a static search tree (S+ tree) in Rust for high-throughput queries over a sorted array of 32-bit unsigned integers, returning the smallest element >= q. Starting from Algorithmica's S+ tree baseline, the author reports reaching roughly 40x the throughput of the Rust standard library binary search on large out-of-cache inputs, with the Eytzinger layout alone giving about 4x. The core techniques are: 64-byte cache-line nodes of 16 u32 (branching factor 17), query batching that exploits the CPU's ~12 line fill buffers to overlap many RAM reads, explicit prefetching of the next child node, and hand-written AVX2 that trims the per-query find down to a vpackssdw + vpmovmskb sequence. Further gains come from byte-based pointer arithmetic that eliminates shift instructions for the 64-byte stride (17->15 instructions per iteration) and from 2MB hugepages to reduce TLB misses. All measurements are self-reported on the author's i7-10750H laptop with AVX2 only and frequency fixed at 2.6GHz; methodology (median of 5, hugepage rounding to 32MB, 31-bit value assumption) is described, but results are not independently verified. The stated motivation is speeding up suffix-array search for bioinformatics indexing of static reference genomes.

• The problem framing: inference is approaching million-token contexts while RL post-training often stays at 256K tokens or below, forcing reliance on length generalization at deployment; this matters most for agents whose observations, tool outputs, documents, and prior decisions accumulate over long trajectories.
• Core mechanism (three parts): evaluate the shared prompt without autograd, retain only model-specific state needed by later tokens, and replay short response branches one at a time; this shrinks the live training graph in exchange for additional replay time. Instantiated with Group Relative Policy Optimization (GRPO).
• On 8x H20 GPUs with the hybrid recurrent/full-attention Qwen3.6-27B: completes grouped scoring and response backward at 2.1M positions for groups of 2 and 8; scaling the group from 2 to 8 adds only 0.21 GB peak allocated memory. A separate stress test on the same setup reaches 4.46M positions.

LongStraw is an architecture-aware execution stack for million-token RL post-training under a fixed GPU budget, instantiated with GRPO. It addresses the gap between inference systems nearing million-token contexts and RL post-training that typically remains at 256K tokens or below. The method evaluates the shared prompt without autograd, retains only model-specific state needed by later tokens, and replays short response branches sequentially, trading extra replay time for a smaller live training graph. Reported results include grouped scoring and response backward at 2.1M positions on 8 H20 GPUs for the Qwen3.6-27B hybrid recurrent/full-attention model (with a 4.46M-position stress test), and an end-to-end execution path validated for a 2.1M-token prompt across all 78 layers of the compressed-attention MoE GLM-5.2 on 32 H20 GPUs. The authors are explicit that these experiments demonstrate execution capacity rather than training correctness, since the captured prompt state is detached and some distributed forward and gradient composition paths remain incomplete.