半形式化方法加速数学验证

We need tools for good verification. Mathematics is the best domain for tests here as we already have formal Lean mathematics that can be well verified.

However Lean formalization is often expensive and long (even with autoformalization tools, which add potentially more problems, like translations' faithfulness), and in many cases out of reach because we lack a particular domain in mathlib for example.

Having semi-formalization, or pseudo-formalization like in this paper below, is one way to make this process faster. Not as bulletproof as Lean-formalization, but good enough to know where potential challenges with a proof might lie.