Scott Armstrong publishes skill files for LLM-driven Lean autoformalization