Joachim Neu

I maintain this website of upcoming deadlines for academic venues relevant to blockchain research: blockchain-deadlines.github.… About a year ago, I started using a Python script and the OpenAI API to keep the site up to date. nitter.cf/i/status/1868995269691… Today ... 🧵

Idk who needs to hear this, but formal verification of software (mathematically checking that software is correct) is by no means done, even now that we have LLMs and the proof tedium is gone. Instead, having LLMs lets us focus on the spec, where humans remain in the loop, and where people were often sloppy in the past. By sloppy I mean they often touted “formally verified!!11”, without even mentioning the spec. And upon closer inspection, the spec often turned out to miss critical guarantees you would naturally expect. Formal verification IS hard. First, you need to figure out what behavior you even want to check: the spec. Then, you need to go through the tedium of writing a proof that your program indeed satisfies the spec. LLMs massively speed up the second step. That’s because the proof can automatically be checked by a compiler. If the compiler is happy, the LLM did its job and you can trust the result, namely that your program satisfies the spec, without reading the proof yourself. (Ofc assuming you don't hit a compiler bug.) But the first step is still there: What’s the spec? Writing the spec is still tedious and error-prone, and while LLMs help, a human needs to remain in the loop, at least to some extent, to assess whether the spec matches with the programmer's intention and the user's expectation. If you vibe that part, that’s where the bugs will creep back in. Also: not all specs are equal. Don't trust "formally verified" without checking the spec. If the spec only says "the program doesn't crash", that is much less useful than a spec that reflects in detail the intended and expected functionality of the program. So, humans are not leaving the loop, we're just moving up a level. With the proof tedium gone, we can finally focus our attention on the spec!

TIL there are many different games now to learn Lean. So cool! adam.math.hhu.de/

I can't believe how cheap and simple this has become: in my experience, mechanizing a research paper in Lean, one-shot end-to-end from the English draft, now costs on the order of $20. Here are my order-of-magnitude ballparks based on the papers we've auto-mechanized so far: 1 page of paper ~ 1k LOC of Lean. 1 LOC of Lean ~ $0.01 in API pricing. And tokens as part of a subscription seem to be ~10x cheaper than API (many say >20x; but let's be conservative). So a 20-page paper ~ 20k LOC ~ $200 API ~ $20 equivalent on a Claude plan. => A $100/month plan should mechanize ~5 papers per month. Our first mechanization, on Erdős problem #320 w @skominers, cost ~$2k for ~30k LOC — 7x above ballpark. Paper: scottkom.com/assets/articles… Code: github.com/joachimneu/distin… To get the cost down, don't run the strongest model on max effort throughout (that's what we did in the $2k version). Have Fable (high effort is enough) act as orchestrator: it lays down the scaffold — definitions, lemma statements, file structure — and dispatches Sonnet subagents to fill in the proofs. Seems Sonnet is enough for that: 17/17 proof files on first dispatch in our latest run, zero escalations (allow the model to upgrade subagents to Opus/Fable if Sonnet is struggling). So: mechanizing your paper probably costs 1-2 orders of magnitude less than the registration fee of the conference you'd submit it to. How far are we from venues asking for a mechanization alongside the submission?

Daydreaming about Lean ...

Some big AI gains in my daily research process come from an unglamorous place: the "mechanical" aspects of paper production. Digesting reviews: The AI reads the paper, the related works, and all the reviews, and distills the reviewers' top grievances; deduplicated across reviewers, ranked, mapped to where in the paper they arise, likely misunderstandings flagged as such. Great starting point for the rebuttal, and later for revision or cam-ready! Camera-ready: Drop those 20 page publisher's "author instructions" PDFs (of course we all read those, right? ;)) into the context, together with the paper's LaTeX, and the AI works thru the checklists (ORCiDs, template compliance, reference formatting, ...). A particularly interesting step sits between, though: deciding what to actually do about each point of the reviews/rebuttal. Usually that's discussed among coauthors in a call or at a whiteboard. Turns out, if you record that conversation (eg, on Zoom, so you get a transcript for free), and take a high-res photo of the whiteboard at the end, the AI gets a very good understanding of what was discussed and decided. (You can instruct AI to match transcript timestamps to video frames using ffmpeg.) From there, it can already make many (in my experience 80-90%) of the edits itself. I am quite optimistic about this pattern: the AI takes over the grunt work, leaving the humans more time for thinking, wondering, discussing, etc (the fun part). I'm setting up a new office @TechnionLive soon, and I want this workflow to be routine there: camera on the whiteboard and a room mic permanently in place, recording starts w one button, files stored where all meeting participants can access them afterwards. (The recording is only useful if it ends up in everyone's repo and AI context.) Anyone already have a room like this? What gear did you end up with? (Esp. for high-res whiteboard photos.) Where do the files go?

Curious what other researchers' AI setups/workflows look like. Here's mine: Everything pertaining to one research project lives in one git repo: the paper's LaTeX, experiment code, Lean mechanization, related works, reviews and rebuttal, research notes, even meeting recordings and whiteboard photos. Inside the repo sits a devcontainer, and inside that runs Claude Code. VS Code makes devcontainers seamless. Sandboxed like this, I can let it run with permissions skipped and not worry about my machine. To access OpenAI models, I have Claude Code prepare prompts and query the models thru github.com/joachimneu/gptpro…. I seed the repo from a template that contains devcontainer config, Claude skills, a library of common LaTeX preamble code, etc. The repo isn't just organization. The point is that the AI can operate on the full context of a project, not just the file I happen to be editing. It drafts the rebuttal having read the reviews and the paper. It writes a paper section having seen the whiteboard photo from the meeting where we outlined it. (The meeting-recording part surprised me the most, that one deserves its own post.) What's your setup? Where/how do you store the large video/image files? Git LFS? Hosted where?

The @commonwarexyz code base has been a great resource (and accelerant) for this project indeed!

... it seems all the necessary capabilities (search, fetch) have been integrated into Claude/Cursor/Codex/Copilot and there is no more need for my self-made Python harness around the OpenAI API. So, I have switched to Claude skills github.com/blockchain-deadli… Seems to work well! :)