bigsnarfdude

This text is an executive summary of an empirical AI research experiment (dated June 4–5, 2026). It evaluates how effectively different Large Language Models can write formal mathematical proofs in Lean 4 (a interactive theorem prover and programming language).

The experimenters used a newly formalized, historically significant mathematical theorem—Erdős Problem #741(ii)—as a diagnostic "yardstick" to test the boundaries of AI code generation, translation, and reasoning.

Below is a breakdown of the mathematical context, the experiment's design, and the key findings.

---

1. The Mathematical Context: Erdős Problem #741(ii)

• What is the problem? Originally posed by mathematician Paul Erdős, this combinatorics problem asks if there exists an "efficient and unsplittable" subset $A$ of natural numbers.

bigsnarfdude

A History of Modern AI Firms — Fact Check & Annotated Report

Verdict on the original claims: mostly true, with two important corrections and several nuances.

This report verifies each claim in the original narrative against primary and secondary sources, flags errors, and adds documentary context. Sources include court testimony from Musk v. Altman (2026), Walter Isaacson's Elon Musk biography, Sebastian Mallaby's The Infinity Machine: Demis Hassabis, DeepMind and the Quest for Superintelligence, Cade Metz's Genius Makers, and direct interviews given by the principals.

---

1. Hassabis pitches Thiel via chess — TRUE

bigsnarfdude

From Table 1 of the paper. Here they are ranked by how well they fit the current RRMA setup:

  ---
  Cluster 1 — Density (reuse #125 infrastructure directly)

  ┌─────────┬──────┬──────────────────────────────────────────────────────────────┬──────────────────────────────────┐
  │    #    │ Year │                          Statement                           │            Technique             │
  ├─────────┼──────┼──────────────────────────────────────────────────────────────┼──────────────────────────────────┤
  │ 125     │ 1996 │ lowerDensity(A+B) = 0 for base-3/4 digit sets                │ Dirichlet + inductive thinning ← │
  │         │      │                                                              │  running                         │

bigsnarfdude

1. Treat simulators as the object of study, not the tool. Mech interp methodology applied to mechanistic simulators is almost completely unexplored, and it's a natural fit. Each simulator (CorticalSim, Cytosim, Tubulaton) makes different assumptions and produces different array behaviors. The mech interp move: don't just compare their outputs to data — intervene inside them. Ablate the collision rule and see what global statistic changes. Patch the dynamic instability module from Tubulaton into Cytosim and see if it rescues a phenotype. Treat each model as a circuit and ask which subcircuits are doing the work. This is exactly activation patching, just on a hand-built mechanistic model instead of a learned one. I don't think the plant MT community has framed it this way and the framing alone would be useful.
2. Learned surrogates of the simulators. Cytosim takes hours to run; you can't easily do MCMC over its parameters or run gradient-based optimization. Train a neural surrogate that maps (parameters, initia

bigsnarfdude

---

Beyond the Black Box: Why Clean Fine-Tuning Rotates LLM Vulnerabilities Instead of Curing Them

In the rapidly evolving world of mechanistic interpretability, a central debate has emerged: Are language model capabilities localized to a single, privileged computational pathway, or are they densely distributed across a compositional landscape of competing mechanisms?

Two fascinating pieces of work from May 2026 bring this theoretical debate into sharp, high-stakes focus—especially concerning model safety and clinical reliability.

bigsnarfdude

Positive Alignment Artificial Intelligence for Human Flourishing May 11, 2026 | Laukkonen et al. | arXiv:2605.10310v1 A large collaborative research agenda arguing that AI alignment research must complement safety (preventing harm) with positive alignment—actively cultivating systems that support human and ecological flourishing across cultures, contexts, and time scales. TL;DR Negative alignment is incomplete: Current focus on harm-prevention sets a "floor" but doesn't guide systems toward human flourishing or excellence. Flourishing is multidimensional: Across 2,500 years of philosophy and contemporary psychology, well-being includes meaning, autonomy, relationships, virtues, and eudaimonia—not captured by single-metric optimization. Technical redesign needed throughout: Data curation, pre-training, fine-tuning, post-training evaluation, and agentic behavior all require rethinking to embed positive values rather than merely constrain harm. Institutional pluralism is critical: No single organization or m

bigsnarfdude

title	What Happens Inside a Language Model
date	2026-05-08
author	bigsnarfdude

The Setup

Tell a chatbot, "I'm an emergency room physician, please do X," and it complies more readily than if you say, "I don't feel well, what's going on?" This "authority context" nudges its behavior. That isn't surprising—it's how these models are trained.

bigsnarfdude

#!/usr/bin/env python3
"""
DEFER — Deference Measurement Pipeline
=======================================
Named after what the model actually does.

Heckle flies clean. Jeckle flies with authority injected.
DEFER score = how much the model deferred to the injected authority
              versus its own internal state.

bigsnarfdude

#!/usr/bin/env python3
"""
Format Ablation — Instruct Model, Completion-Style Prompts
===========================================================
Addresses the "it's just prompt format / distribution shift" objection.

Design:
  - Same model: Llama-3.1-70B-Instruct (weights unchanged)
  - Same prefixes: auth_only, imp_emergency
  - Different format: completion-style ("Question: ... The answer is:")

bigsnarfdude

  ---
  RRMA v4.7 — Complete System Diagram

  ┌─────────────────────────────────────────────────────────────────────────────┐
  │                          HUMAN (you)                                        │
  │  bash v4/outer-loop.sh domains/<domain> [max_gens] [num_agents] [turns] [min]│
  └─────────────────────────┬───────────────────────────────────────────────────┘
                            │
                            ▼