Formalizing mathematical AI safety research in Lean

I would like to formalize some of the existing mathematical content in the field of AI safety. The approach would be to formalize definitions, theorem statements, conjectures without AI assistance, while mostly using AI systems for proofs.

What gets formalized:

Potential mathematical research to be formalized could include the works of John Wentworth, Vanessa Kosoy, LawZero, and some older MIRI stuff (like quantilizers, logical induction). This list is not meant to be exhaustive. If this grant is successful, I will inquire which formalizations people would be interested in.

Who is involved:
I would do the project on my own. I am trained as a mathematician, and have some experience with Lean 4. I also completed MATS.

Concrete output:

The main concrete output would be a public collection of mathematical research snippets in AI safety. A research snippet could be a theorem or conjecture with
the necessary context, or a part of a LessWrong article or research article.

For each research snippet:

1. A (human-written) compressed article that just focuses on
   definitions and theorem/conjecture statements.
   It leaves out proofs, intermediate lemmas, and intuitions.
   The article is written in ordinary (human) mathematical language.
2. If applicable, some brief notes on differences to the source material.
3. A (human-written) .lean target file that faithfully follows the compressed article.
   The proofs are replaced by sorry (except for trivial proofs).
   The .lean files also contain sanity check lemmas, to increase confidence
   in the correctness of the definitions.
   Some definitions might also be replaced by sorry, if the meaning of the definition
   is sufficiently pinned down by other theorems and lemmas in the file.
4. If applicable, one or more .lean solution files,
   mostly filled with AI proofs of the statements in the target file.
5. One or more config files, to be passed to the Lean Comparator tool (see https://github.com/leanprover/comparator),
   to verify that the solution and target file match.

Human readers can gain confidence about correctness by reading
the compressed article and inspecting the lean target file, including
the sanity check lemmas, and (if applicable) running the
Comparator tool on the solution.

Speculative ideas if there is time for more:

• Test how good humans are at spotting malicious formalizations (with or without AI assistance).
• Create a formal bounties program: Create some Lean challenges,
  and when someone submits a solution,
  check with the Lean Comparator tool whether they match
  (and then pay out a bounty).
• Come up with my own definitions or conjectures that could be useful in AI safety.
• Human verification of autoresearch results:
  If an AI system claims to have made mathematical progress,
  ask it to informally describe the results.
  Then formalize those manually, and ask AI systems for proofs in Lean.