A branch of research that involves using automation such as AI/LLMs to generate formal mathematical proofs. The field is primarily focused on doing this for actual math problems/papers, but it feels very adjacent to us especially if you take the view that legal documents are computer programs that happen to be written in natural language.