Comment by nbulka

If you’ve tried any formalizing in codex Astra often works solely in Lean