I recently spent 3 weeks with claude formalizing a CS paper about a borrow checker in lean, for a personal project.

The formalization went through, but there were _several_ mistakes in the original paper that it uncovered, from type setting errors to (many) formulas that quantified over all resources as printed, but actually applied to only arising resources in the calculus..

So the formalization did give me a formally verified borrow checker that I could use to build a programming language on top of, but it was _not_ exactly the borrow calculus that was printed in the paper.

I expect this is the most common experience when mechanizing a printed paper. There are a lot of skipped steps and handwaving.

▲ ted_dunning 6 hours ago | parent | next [-]

This is the common experience in replicating a published paper by hand ... it is common to find "obvious" aspects that are anything but.

The scary thing is when AIs generate unreadable formal proofs and then effectively lie (or fabulate, to be polite-ish) about the natural language version of the steps. Since the natural language version is arguably the most important aspect of a solution to a flagship problem, this fabulation deflates the value of the solution while the existence of the solution discourages further work on the problem.

	▲	ndriscoll 5 hours ago \| parent [-]
		I have hopes that this is primarily a matter of needing more engineering work on ergonomic formal languages and better building a language that "looks like math." e.g. when doing linear algebra stuff, a linear combination might be defined as a finitely supported function from an index set to your space, which is fine, but ugly and maybe conceptually overwhelming on first meeting, so I did some toying with little macros and eventually a small python Lean -> HTML renderer to do some basic transformations to make it look more like typical math notation with like \Sigma_{i \in I} a_i, or with a_0+...+a_n, etc. (to... not fantastic success, but I think there's still something to the idea). I think a lot of math notation isn't wrong given a context, so in theory we should be able to translate it into something formal. Maybe also generate living documents where you can e.g. write `h : some_claim := by details(by rw[nat_mul_comm]; ...)` and the renderer hides details just like you'd write "obviously" in a traditional text. If the reader wants, they could then expand the details. etc. I found that many codex-generated proofs could be improved by telling it that I want a sequence of steps `have next_step := by <I don't care> have therefore := by <still don't care>` So that the human proof appears as the left side, and I just ignore the right side as petty details. Again, not fantastic success, but better. Otherwise it goes very... Leanish by default. Lean's VSCode plugin is I think only starting to explore the idea of a proper IDE for math. There's probably still tons of unexplored potential for like that fused with Matlab or whatever.

▲ hgoel 5 hours ago | parent | prev | next [-]

I enjoy running into those details when implementing papers, since it usually leads to improved understanding of the subject and an ability to approach the matter with more rigor in some way that I had not noticed before. It does also involve a lot of work and lost sleep though.

We should be very careful about relinquishing sorting through such details to AI.

	▲	empath75 3 hours ago \| parent [-]
		Claude could not fix them without a lot of help, so i did not relinquish sorting through those details in general. Just the drudgery of grinding through proof obligations.

▲ dekhn 6 hours ago | parent | prev [-]

As a second rate scientist, nothing makes me happier than finding a "hot" paper in my field, reading it, converting it to code, and demonstrating the authors made systematic errors that mean the paper is more likely false than true.

I've been criticized for doing this, but to me it emphasizes how much attention goes to the hot, wrong papers.