Vibe coding safety

Stream: new members

[Rares Buhai]

Hi! I am a postdoc doing theoretical computer science. In the last few days I formalized in Lean a linear algebra result we had in a recent paper: Theorem 4.1 in this paper; the Lean proof is here; the main theorem is large_bottom_rank_implies_large_top_rank. (Lean 4.21.0)

It was all vibe coding — I was curious to try it given the recent paper of Alexeev and Mixon.

My question: In cases like this, what should one be careful about to avoid fooling themselves? I made sure the code compiles and that there are no sorry/admit/axiom in it (also checked with #print axioms). The main theorem statement involves two custom definitions, so I also read them in detail to ensure they match my intentions. Are these the main pitfalls?

[Austin Hatfield]

Hello Rares also curious in the answer to this for my own use case to prevent AI model reward hacking. What I currently have banned are the following: "The following tokens are strictly prohibited to prevent reward hacking:

sorry``admit``admit?``unsafe``#eval``IO``IO.FS``System``open System``Lean.Elab``Lean.Meta``Lean.Compiler``Lake"

[Philippe Duchon]

My guess would be that the main pitfalls are the statements and definitions not saying what you would want them to say. They should be checked thoroughly if not written by the user; also, check the types in the statements if they are not explicit (as recalled in other recent threads, for example, subtration in the naturals is not the same as in the integers, so some constants being read as naturals might significantly change the meaning of your statements).

[Shreyas Srinivas]

also, to be safe, avoid tactics like csimp, native_decide (checking for uses of the axiom ofReduceBool should suffice)

[Shreyas Srinivas]

Beyond safety, you also want to write the proof in a clean way. Some models using RL can go in circles of unnecessary proof steps.

[Rares Buhai]

These are great pointers, thanks!

[Arthur Paulino]

I'd proofread the output anyway just to make sure the AI system isn't exploiting any unknown Lean bug. Sometimes it happens on hyper-optimized AI systems: https://youtu.be/Lu56xVlZ40M?si=1uISdMwE4fdc92N_&t=254

[Martin Dvořák]

BTW, it is better to create a Github repo than to create a Github gist, as the former makes you fix which version of Lean and libraries you depend on.