This is an interesting approach.
My team has been prototyping something very similar with encoding business operations policies with LEAN. We have some internal knowledge bases (google docs / wiki pages) that we first convert to LEAN using LLMs.
Then we run the solver to verify consistency.
When a wiki page is changed, the process is run again and it's essentially a linter for process.
Can't say it moved beyond the prototyping stage though, since the LEAN conversion does require some engineers to look through it at least.
But a promising approach indeed, especially when you have a domain that requires tight legal / financial compliance.
The autoformalization gap is pretty difficult to bridge indeed. We explored uncertainty quantification of autoformalization on well-defined grammars in our NeurIPS 2025 paper : https://arxiv.org/abs/2505.20047 .
If you ever feel like chatting and discussing more details, happy to chat!
Could you share an example of such policy? I'm struggling to think of something defined well enough in the real world to apply in Lean.
For anyone curious about what LEAN is, like me, here’s the explanation: Lean Theorem Prover is a Microsoft project. You can find it here: https://www.microsoft.com/en-us/research/project/lean/
Lean has been under development over the last 13 years, part of that while chief architect Leo de Moura was employed by Microsoft Research (he's now at AWS). However, Lean is an open source project, not exclusively a Microsoft project. More accurately, see here: https://lean-lang.org/
That’s pretty cool. It would be super useful to identify contradictory guidance systematically.