Sure, what the program does is not interesting by itself, neither is that you can use AI to create programs to do polygon intersection.
The main feature, that I hope is interesting in this submission, is that the program is formally verified and how I used formal verification together with AI to create it.
Formal verification means that a mathematical proof is provided that the program satisfies a specification. And that proof is checked automatically by a deterministic system, the lean checker, which we can trust, in constrast to error prone LLMs.
I gave the agent a formal specification m1.interior ∩ m2.interior = result.interior and it produced an implementation together with such a formal proof. With this approach we can treat much of the work of the agent as a black box, which we don't have to review to judge correctness.
I think the project shows that as AI agents get more capable, an approach like this is starting to get practical for certain problems like polygon intersection for which there is a concise way to specify the problem.
The main feature, that I hope is interesting in this submission, is that the program is formally verified and how I used formal verification together with AI to create it.
Formal verification means that a mathematical proof is provided that the program satisfies a specification. And that proof is checked automatically by a deterministic system, the lean checker, which we can trust, in constrast to error prone LLMs.
I gave the agent a formal specification m1.interior ∩ m2.interior = result.interior and it produced an implementation together with such a formal proof. With this approach we can treat much of the work of the agent as a black box, which we don't have to review to judge correctness.
I think the project shows that as AI agents get more capable, an approach like this is starting to get practical for certain problems like polygon intersection for which there is a concise way to specify the problem.