Library
Papers and posts ingested into the system, each with synthesis notes. Grouped by publication year.
2026
- When AI builds itself post First-party evidence that AI development is automating from execution upward: implementation and fixed-goal experimentation have accelerated sharply, while problem choice, review, and verification remain the binding constraints—not yet a closed recursive self-improvement loop.
- A digestion of the proof of Sendov’s conjecture Aug · post An AI-generated, Lean-certified resolution of Sendov's conjecture arrived correct but unreadable; Tao's several-day human+AI digestion — tracing each identity to classical literature, simplifying to an elementary argument, re-formalizing at a sixth the size — shows the bottleneck moving from verification to understanding.
- CAKE: Compiler-Agent Co-Design for Frontier Kernel Evolution paper Co-design flips the kernel-agent question — a fixed agent against an evolving, agent-facing compiler instead of a better agent against a black box — and the matched clean-start experiment credits the environment locus alone with turning 0.93× into 1.14× over a tuned baseline.
- Learning more about Claude's mathematical capabilities post A failed attack on the Riemann hypothesis produced a narrower bound by composing earlier mathematics at massive agentic-search scale, with human review and Lean checking supplying evidence but not an independent statement-fidelity audit.
- MatrAIx: Simulating the World with 8.3 Billion Persona Agents paper MatrAIx makes the product rather than the agent the system under test and gives simulated-user studies auditable cohort, task, trace, and verifier contracts, but its own evidence supports hypothesis generation rather than substitution for real populations.
- Forbench: Symbolic Simulation Helps Make Your Testbench More Formal paper Fork on testbench conditions, not design branches: a symbolic-simulation runtime with simulation ergonomics — real engineering value, though the 'third path' framing oversells its distance from prior symbolic simulation.
- Postmortem for Kernel Soundness Bug #14576 post A model postmortem quantifying the residual risk behind 'the kernel checked it': soundness now requires two independent bugs to fail, elaborators must stay untrusted — and models strong enough to find soundness bugs change the threat model.
- Ten advances in mathematics and theoretical computer science post The evidentiary weight rests entirely on Lean certificates neutralizing corporate-claim skepticism — modulo statement fidelity — and the disclosed workflow is draft-sketch-prove's shape at research scale.
- Memory for Large Language Models Jul · paper The durable map separates compute-coupled state from independently operated storage, then asks when memory changes and how long its influence survives; the map is more convincing than its treatment of static MoE experts as explicit memory or its undocumented survey method.
- The Therapist Pattern post Identity as an evolution locus with a receipt rule: a claimed lesson counts only when it lands in a versioned, inspectable surface through the designated writer — 'I'll remember that' is a red flag, a diff is evidence.
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier paper The solver regime is saturated and its benchmarks exhausted; the frontier is research agents — with specification fidelity and the SMT-vs-CAS verification gap as the load-bearing distinctions.
- A Taxonomy of Self-evolving Agents post Two additive cuts on gao2025's survey: the artifact as a first-class evolution locus, and 'where does the loop close' as the deployment-facing question.
- Harness Engineering for Self-Improvement post A researcher's opinionated map of the harness level: evaluation and permissions must live outside the self-modification loop, and harness functions will internalize into models while interfaces persist.
- Scaling Laws, Carefully Jun · post Scaling laws are extrapolation instruments, not universal constants: their value comes from regime-specific empirical regularity, while parameter counting, fit range, optimizer termination, numerical precision, and finite-data repetition can materially move the inferred compute-optimal frontier.
- Superpowers 6 post The most concrete public numbers yet for a self-improving harness — promotion gated by evals outside the loop, negative results logged — and the Codex-isolation lesson: the evaluator is code too, and an unverified gate passes everything.
- Improving Equality Saturation for EDA via Semantic E-Graphs paper Semantic e-graphs make domain meaning part of e-class identity, letting Nextmap retain word-level, bit-level, optimization, and mapping alternatives in one search structure; the ablations support the cost of premature extraction, while soundness and commercial-competitiveness claims remain conditional on user-supplied equalities and a resource-focused evaluation contract.
- Self-Harness: Harnesses That Improve Themselves paper The loop architecture — evidence before proposal, bounded surfaces, conservative gating — survives scrutiny; the headline gains, measured against a floor baseline with a reused held-out split, do not.
- Loop Engineering post Practitioner naming of the layer above the harness — five now-converged product primitives plus external state turn agent-prompting into a designed system — with the honest concession that the loop amplifies the operator's judgment or its absence.
- LLM Wiki Apr · post The wiki compiles understanding rather than retrieving it, and the LLM pays the maintenance cost that historically killed personal wikis — structural claims that outlive the tool roster.
- Mathematical methods and human thought in the age of AI Mar · paper The shelf's missing philosophical frame: AI's genuine novelty is decoupling the outward form of intellectual products from the thought that made them, and the essay's vocabulary — smell, odorless proofs, the red-team asymmetry, a Copernican view of intelligence — names what the practice entries instantiate.
2025
- LLM4SCREENLIT: Recommendations on Assessing the Performance of Large Language Models for Screening Literature in Systematic Reviews Nov · paper Under screening's extreme class imbalance Accuracy rewards rejecting everything and even chance-anchored MCC still picks models that lose half the evidence — so publish the full confusion matrix, headline Lost Evidence, and rank by cost-weighted WMCC with the FN:FP weight declared and justified.
- Olympiad-level formal mathematical reasoning with reinforcement learning paper AlphaProof is verifier-grounded RL at AlphaZero scale plus test-time RL on problem variants — IMO silver at a compute scale beyond academia, with competition math's fixed concept library marking where research mathematics begins.
- Dual-Model LLM Ensemble via Web Chat Interfaces Reaches Near-Perfect Sensitivity for Systematic-Review Screening: A Multi-Domain Validation with Equivalence to API Access paper OR-ensembling two model families buys near-perfect screening sensitivity because each model's errors are systematic and repeat across its own runs (κ 0.78–0.93), so diversity must come from outside the model — but no same-family ensemble arm was run, and the headline number rests on LLM-triggered relabeling of the reference standard.
- Superpowers: How I'm using coding agents in October 2025 Oct · post The academic shelf's safeguards discovered independently by iteration — plus the 2,249-memories null result: most accumulated lessons are already absorbed, so an earned-lesson filter is the main mechanism, not optional caution.
- Agentic Context Engineering: Evolving Contexts for Self-Improving Language Models paper Contexts should grow as itemized, provenance-counted entries with deterministic merges — brevity bias and context collapse name why blob rewrites fail, and feedback quality binds any self-updating context.
- My AI Had Already Fixed the Code Before I Saw It Aug · post Named the philosophy: each unit of engineering should make the next cheaper, and agents close the feedback loop cheaply enough for the compounding to actually happen.
- FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution paper FuSS spends fuzzing on broad concrete exploration and symbolic execution only on short suffixes beyond a coverage frontier, producing strong branch and toggle coverage curves without turning coverage into a proof or supporting its unconditional always-faster claim.
- A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence Jul · paper A usable field map — experience-dependent, persistent, self-initiated updates define self-evolution, and the safety checklist transfers as-is to memory-carrying agents — though the ASI framing writes a check the content never cashes.
- How is Modular Democratizing AI Compute? (Democratizing AI Compute, Part 11) Jun · post The proposed CUDA successor is a vertically coherent but independently usable stack—Mojo for kernels, MAX for model execution and serving, and Mammoth for clusters—whose portability thesis is clearer than the self-graded evidence offered for its product claims.
- AlphaEvolve: A coding agent for scientific and algorithmic discovery paper Evolution as the harness that converts test-time compute into discovery: only executed, scored code persists, sidestepping hallucination — within evaluator reach, and only there.
- The lethal trifecta for AI agents: private data, untrusted content, and external communication post Agent risk becomes structurally acute when one execution path combines private-data access, attacker-controlled input, and an exfiltration channel; the robust control is to break that capability triangle rather than trust probabilistic prompt defenses.
- Modular’s bet to break out of the Matrix (Democratizing AI Compute, Part 10) May · post Modular presents itself as an institution designed around the six prerequisites for industry-scale change, but its account of aligned incentives and patient closed R&D is a founder's causal narrative whose technical success claims remain largely self-attested.
- Why do HW companies struggle to build AI software? (Democratizing AI Compute, Part 9) Apr · post AI-accelerator competition is an organizational and ecosystem problem before it is a chip-design problem: hardware differentiation multiplies the software burden while incumbent-focused community work compounds NVIDIA's advantage.
- What about the MLIR compiler infrastructure? (Democratizing AI Compute, Part 8) post MLIR succeeded as shared infrastructure for building heterogeneous compilers, but its dialect extensibility could not itself supply the product leadership, reference stack, or aligned incentives needed to unify AI software.
- What about Triton and Python eDSLs? (Democratizing AI Compute, Part 7) Mar · post Python eDSLs make custom GPU kernels approachable by reusing Python syntax and raising execution to blocks, but Triton's apparent portability stops at an abstraction boundary where hardware generations, debugging, and peak performance still demand target-specific knowledge.
- What about TVM, XLA, and AI compilers? (Democratizing AI Compute, Part 6) post TVM and XLA show why automatic kernel generation and model partitioning are necessary but insufficient: fixed operator abstractions gain leverage over workload combinations while losing the hardware control and organizational alignment demanded by new accelerators.
- What about OpenCL and CUDA C++ alternatives? (Democratizing AI Compute, Part 5) post OpenCL's mixed outcome suggests that portable accelerator software needs a fast-moving reference implementation and access to differentiated hardware, but Lattner's governance diagnosis is stronger than his unsupported performance and vendor-intent claims.
- CUDA is the incumbent, but is it any good? (Democratizing AI Compute, Part 4) Feb · post CUDA has no context-free quality verdict: its mature ecosystem helps application developers, its low-level control taxes performance engineers, its vendor boundary blocks portable software, and its accumulated compatibility burden may constrain NVIDIA itself.
- How did CUDA succeed? (Democratizing AI Compute, Part 3) post CUDA's dominance is explained as a compounding platform flywheel: a broad compatible install base attracts developers, vendor-maintained libraries bind frameworks to new hardware, and CUDA-first research and capital spending make the next cycle still more NVIDIA-specific.
- What exactly is “CUDA”? (Democratizing AI Compute, Part 2) post CUDA is most usefully understood as a vertically integrated platform—driver, programming model, optimized libraries, and application-level solutions—whose accumulated layers explain both its leverage and the difficulty of replacing it.
- DeepSeek's Impact on AI (Democratizing AI Compute, Part 1) Jan · post DeepSeek is used less as an object of technical analysis than as a forcing event for a platform thesis: cheaper model execution should enlarge AI demand, making hardware utilization, portability, and developer access more important rather than less.
2024
- Disjoint projected enumeration for SAT and SMT without blocking clauses Apr · paper TabularAllSAT and TabularAllSMT combine CDCL, chronological backtracking, and implicant shrinking to enumerate a disjoint projected cover without accumulating blocking clauses, trading complete tuples for compact partial models.
- Benchmarking Human–AI collaboration for common evidence appraisal tools Sep · paper Put the human gate at human–LLM disagreement: scoring only items where one human rater and an LLM agree beat both solo humans and LLM ensembles on PRISMA/AMSTAR, but on PRECIS-2 — where humans themselves barely agree — the same design deferred three-quarters of the work, so the collaboration pattern, not the model, carries the result, and human inter-rater reliability bounds it.
- My Personal Journey in Verification Jul · post Hardware verification quality grew by adding complementary failure detectors—formal contracts, cover and induction, configuration sweeps, integration tooling, mutation and code coverage, and self-checking simulation—because each apparently complete method left a different blind spot.
- A forest of evergreen notes Jun · post A tour of Forester separates note content, reusable format, authorship, and publishing posture into independent design choices, dissolving a simple Zettelkasten-versus-wiki binary.
- Solving olympiad geometry without human demonstrations Jan · paper AlphaGeometry makes the neural-proposes/symbolic-closes split architectural and answers data scarcity with synthetic data from symbolic exploration — but the claim's scope lives in the DSL's translation layer.
2023
- Directed Test Generation for Hardware Validation: A Survey Dec · paper Directed hardware testing is best understood as a target-and-contract layer spanning formal, concolic, statistical, learning, constrained-random, and ATPG mechanisms; this survey maps that breadth well, but its search method and family-level tradeoff ratings are not reproducible measurements.
- Cryptol, SAW, and the Galois Origin Story Nov · post Cryptol and SAW form a specification-to-implementation bridge: executable cryptographic models are compared with lifted software or hardware IR, letting one verification architecture span source languages, optimized code, and RTL while concentrating trust in the lifting and proof chain.
- Voyager: An Open-Ended Embodied Agent with Large Language Models May · paper The founding exemplar of skill-library evolution: verification before persistence, frontier-aware task proposal, and skills indexed by purpose — demonstrated against notably handicapped baselines.
2022
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Oct · paper Draft–sketch–prove operationalizes Wiedijk's proof sketches: neural proposes structure, symbolic closes rigor — the division of labor every informal-guided prover since inherits.
2021
- The PRISMA 2020 statement: an updated guideline for reporting systematic reviews Mar · paper Reporting as the enforceable surface of review quality: 27 items whose common thread is that everything — search, near-miss exclusions, automation, competing interests, data and code — is disclosed somewhere a reader can check.
2020
- Generative Language Modeling for Automated Theorem Proving Sep · paper GPT-f set the recipe modern provers still run — tactic generation as language modeling, verifier-coupled search, expert iteration — with community-merged proofs as the adoption bar.
2019
- How can we develop transformative tools for thought? Oct · post Transformative tools for thought require an insight-through-making research culture: the tool must generate new understanding of its subject while that understanding recursively changes the medium, under incentives that ordinary product development rarely supplies.
- Why Don't People Use Formal Methods? Jan · post Formal-methods adoption is not one cost curve: full code verification faces proof and specification costs, while design verification is technically lighter but socially detached from executable code and ordinary development workflows.
- Under the hood of Formal Verification post Open-source RTL formal verification turns assertions and cover goals into solver problems, while richer temporal assertions compile through automata whose determinization makes the hidden state-space cost concrete.
2017
- Research Debt Mar · paper Research debt is accumulated missing interpretive labor: weak exposition, undigested ideas, poor formalisms, and noise make every future reader repay costs that one deep act of distillation could have amortized.
2016
- A Survey of Symbolic Execution Techniques May · paper Symbolic execution is an architecture of tradeoffs across execution mode, memory and environment models, path-space control, and solver strategy; practical engines move complexity between paths, formulas, models, and concretizations rather than eliminating it.
2015
- MultiSE: Multi-Path Symbolic Execution using Value Summaries Aug · paper MultiSE represents one consolidated execution as per-variable sets of guarded values, making path sharing incremental and explicit; its prototype shows large speedups on small JavaScript harnesses, but the comparison does not establish that path explosion is solved or that conventional merging must lose paths.
- All-Solution Satisfiability Modulo Theories: Applications, Algorithms and Benchmarks paper All-SMT makes the observation coordinates explicit: it enumerates every feasible valuation of designated Boolean variables, while relevant theory values are sampled annotations rather than independently enumerated outputs.
2014
- Guidelines for Snowballing in Systematic Literature Studies and a Replication in Software Engineering May · paper The snowballing canon: citation edges beat search strings because authors cite each other across terminology drift — one found paper suffices to reach the connected cluster, and for extending an existing study snowballing wins by deduction.
2009
- How To Choose a Good Scientific Problem Sep · paper Problem choice is teachable: a two-axis Pareto scheme with life-stage weighting, a three-month commitment rule, and the cloud/problem-C vocabulary for the mid-project reframe.
2008
- Systematic Mapping Studies in Software Engineering Jun · paper The founding SE mapping-study paper: classification over evaluation buys breadth (structure a whole field, quality-unassessed) and the map is a first step toward a review, not a lesser one — with keywording-built schemes that evolve during extraction.
2007
- How to Read a Paper Jul · paper Reading depth is an explicit resource allocation with exit checkpoints, and the re-implementation test is the honest bar for deep reading.
- Guidelines for performing Systematic Literature Reviews in Software Engineering paper The SE systematic-review standard: protocol before review, question-first structure, two-person extraction with measured agreement, documented search with saved raw results — itself gray literature cited five figures deep, and the closest thing the survey layer has to a constitution.
1996
- Reverse search for enumeration Mar · paper Reverse search turns any finite deterministic local search into a parent forest and traverses that forest backward, enumerating without a visited set when parent and adjacency oracles are cheap.
1986
- You and Your Research Mar · paper Problem selection and reframing are trained, scheduled activities, not traits — a control system of allocated attention, compounding effort, and minimized ego taxes.
1981
- Kommunikation mit Zettelkästen: Ein Erfahrungsbericht (Communicating with Slip Boxes: An Empirical Account) paper The missing middle of the compounding-artifact lineage: fixed addresses, explicit links, and surprise as the test of a knowledge system, run for decades at full human maintenance cost.