Cool work. You should make it very loud and clear that your toolchain does not verify proofs, since otherwise folks may think that your computer-assisted proof

Cool work. You should make it very loud and clear that your toolchain does not verify proofs, since otherwise folks may think that your computer-assisted proof layout system does just that; it's rare to see tooling in this subfield which does not verify proofs.