Mathematicians use Lean to verify proofs, whats the equivalent for patent claims

hey! i'm han, one of the cofounders of fearn!

a lot of our inspiration for this approach is based on what’s been going on in math and ai research, especially with the recent news where openai apparently solved erdos’ planar unit distance problem. from what i understand from the ai + math field, ai is being used to search across a really diverse solution space, but for each promising candidate result, a team of mathematicians have to formally verify the solution

as i understand it, mathematicians have been using the functional programming language, Lean, for a while now, to formally verify mathematical proofs. we’re trying to take the same approach, with patent language (and i suspect, this approach could extend to other legal fields). and then i think formal verification could be applied in contexts of program repair or program synthesis, while using ai to explore the patent language space, formally verify, with each iteration