What this project is

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.

Theory of impact

I expect AI systems to improve a lot at formally solving mathematical problems, and they are already quite good at Lean. But it is less clear whether we will be able to
trust advanced AI systems to faithfully formalize statements.
Unlike for proofs, we do not have robust tools for that (and I have already observed claude code occasionally changing definitions to make proving a theorem a simpler task). Just having Lean somewhere in your pipeline does not protect you from slop.

The strategy of human-crafted statements is useful when statements are short compared to proofs.

A big benefit of formal verification is the greater adversarial robustness,
and we lose some of it if we just do autoformalization.

Research progress:

The project could contribute to research progress in agent foundations and other theoretical AI safety areas.

For example, by formalizing conjectures, and then later solving these conjectures with a lot of AI compute. Or by providing formalization services to other researchers.

Gain experience with these systems:

While current systems are only a little adversarial when it comes to formalizing definitions, I think it would be good practice for humans to do definitions and theorem statements in lean without AI assistance.

A big part of the impact of this project could also come from utilizing these skills later in other projects (e.g. the formal bounties idea above).

Shortcomings and Bottlenecks:

Admittedly, the field of theoretical AI safety currently seems to be more bottlenecked by coming up with good definitions and conjectures, rather than solving conjectures. The field is more in the pre-formalization stage, and the difficulties lie more in reducing philosophical questions to concrete mathematical problems, rather than investigating these concrete mathematical problems.
While we would like to prove that some AI systems are somehow "safe", we do not know really have a good mathematical definition of what that means.

Nonetheless, I think there is value in the skills and infrastructure gained by the proposed project, particular when it comes to future capable AI systems
and bridging the trust gap associated with that.

How the money will be spent

Minimum amount 7k USD:
3500 USD/per month, for two months.
Estimated breakdown of the monthly spending:

- 200 USD for AI subscriptions/API costs.
- 3000 USD salary (including taxes)
- 300 USD contingency

Maximum amount 30k USD:

5000 USD/per month, for six months.
Estimated breakdown of the monthly spending:

- 4000 USD salary (including taxes)
- 500 USD for AI subscriptions/API costs, and server costs
- 500 USD contingency and conferences and meeting other researchers.