Library
El universo (que otros llaman la Biblioteca) se compone de un número indefinido, y tal vez infinito, de galerías hexagonales, con vastos pozos de ventilación en el medio, cercados por barandas bajísimas.
Ficciones — Jorge Luis Borges (1941)
Research
-
Essay
A compute operator who claims to have run a particular model can be lying, and the logs that would settle it are written by the party under suspicion. VerInf produces zero-knowledge proofs of LLM inference, bounding the information in an output stream that a committed model does not account for. This living document details what the system certifies, what it does not, and what I contributed to it during the MARS V fellowship.
-
Essay
The actual Hosseini–Mohar–Gonzalez Hermosillo de la Maza stopping tower admits a square-root cop bound in the order of its base whenever the base satisfies the fixed multistage hypotheses used by the earlier occupation transfer. Every ancestry cloud is a retract, so a region that would cost many cops to occupy costs one cop to guard. Fixed port anchors pay for timed retraction setup within the original five-layer accessibility margin. Synchronized setup leaves at most two exceptional clouds, handled by a reusable reserve. The resulting bound has no multiplicative dependence on cloud order or tower scale. A 104-vertex stopped tower shows that the timing gain is a hypothesis and not a consequence of adjacency, and a Hall-capacity inequality shows why full remaining-ball demand stays incompatible with slow growth. The theorem retains the full remaining-ball Hall demand and does not give an all-graphs Meyniel bound.
-
Essay
Ball-Occupation Certificates under Coarse Graph Projections Revised from 27 July 2026
We isolate an abstract strategy-transfer principle for Cops and Robber: a coarse graph projection with bounded fibers and bounded distance distortion lets cops occupy a lifted macro-ball before the robber escapes, giving a quantitative cop-number bound from uniform growth on the base. Applied to the Hosseini-Mohar-Gonzalez Hermosillo de la Maza degree-reduction construction, this gives the known hard family an upper bound within a polylogarithmic factor of the square-root scale. A counting argument then proves a sharp limit on the strategy class itself: Cartesian tori of cycles have bounded doubling and constant cop number but linear occupation cost at every radius, so weak expansion alone cannot certify a universal robustness theorem. The adaptive multistage strategy of Prałat and Wormald does transfer when the base has sphere growth and reservoirs accessible five layers early: for fixed degree, every -occupation projection satisfies , with no logarithm or scale dependence in the cop count. Fixed-degree random regular bases satisfy the strengthened hypothesis with high probability. A companion paper now removes the cloud-order factor for the actual stopping tower under these same fixed multistage hypotheses, using timed cloud guards rather than full-fiber occupation.
Linked the companion timed-guarding theorem, which removes the cloud-order factor for the actual stopping tower under the same fixed multistage hypotheses; reconciled the scope and remaining-demand question.
-
Essay
Proof search is improving faster than the case for trusting it. Proof Broker puts a boundary between the two: Lean and Rocq send a goal out to external provers, take back a certificate with a graded trust tier, verify it at the boundary, and still require a proof term the home kernel checks. Nothing behind the boundary is trusted, so the search behind it can be as aggressive, heterogeneous, or unreliable as finding proofs requires. This essay sets out the architecture, what it makes possible, the evidence so far — 19 of 19 arithmetic obligations closed in a real verification project — and the research program that evidence opens.
Nonfiction
-
Essay
Curricula in mathematics and the sciences optimize for procedural fluency — the half of what they teach that decays once the student stops being a student. What survives twenty years on is conceptual residue, generated only as an accidental byproduct of the curriculum’s intended work. The asymmetry compounds across generations of teachers and produces a population unable to do the work that civic life requires of it.
-
Essay
A compendium of years of informal, empirical experiments aimed at extending the efficacy of Anki beyond rote memorization to more intricate levels of learning.
-
Essay
Notes from Underground is widely admired as a cornerstone of literature, culture, and philosophy. This paper develops the argument that the primary philosophical undercurrent is a rejection of logic and science as end-alls in modern life, traced through comparison with the more explicitly articulated works of Dostoevsky’s contemporaries and successors: Nietzsche, Heidegger, Shestov, Ellul, Sartre, Camus, Husserl, and Arendt.
Poetry
-
Poem
I met a traveller from an antique land, / Who said — “Two vast and trunkless legs of stone / Stand in the desert.”
-
Poem
Like as the waves make towards the pebbled shore, / So do our minutes hasten to their end.
Photography
-
Photo
My study abroad: a time where dreams previous came true, symphonies were written, and new dreams that would define the years to come of my life were born.
-
Photo
A triumphant return to a country I dearly love: a week in Munich, Nuremberg, and Leipzig.
-
Photo
A second, longer stint — after a semester here in 2024. Copenhagen and the places a train reaches from it, added to as they accumulate rather than closed at a date.
AI
-
Essay
Software engineering does so little epistemic work that it hardly earns the name “engineering.” The field has never learned to distinguish provenance — where an artifact came from — from warrant — why anyone is entitled to rely on it. Authorship, a passing test suite, and a completed review are routinely mistaken for the second when they are only ever the first; libraries are the rare exception, where warrant is actually constructed and amortized across users who never read the source. LLM-generated code inherits neither comforting story, and the discomfort that provokes is not a new problem but the oldest one in the profession, finally felt without the anaesthetic that provenance usually supplies.
-
Essay
As we approach AGI, the increase in the ability of Artificial Intelligence models to infer a robust specification from a sparse prompt will lead to a devastating trend of homogeneity. We argue that this is the primary concern regarding the interaction of AI and human intelligence, rather than blanket claims that “AI reduces human cognitive ability.”
-
Essay
AI labs are likely deliberately reluctant to scale because they are aware that any imminient shift to locally run models as the norm would render their compute redundant. We take Anthropic as a principal case study to validate this hypothesis.
Tech
-
Essay
Full Unix-like kernel in ~7,000 lines of C, written for Brown CS 169 (Operating Systems with Lab): virtual memory, VFS, system calls, threading, device drivers and interrupt handlers, and file systems. Custom linker support for running userspace x86-64 ELF binaries.
-
Essay
TCP/IP, RIP, UDP, and DNS implementations in Go, supporting file transmission of up to 1 GB across networks of up to 8 virtual machines. Extended with a fully RFC-compliant SSH implementation (2,000+ additional lines) supporting sustained sessions of arbitrary length.