This issue explores autoformalization and its connection to artificial intelligence. It includes research on converting natural language into formal mathematical representations and improving interpretability. Studies evaluate large language models for reasoning and proofs. The issue highlights challenges and opportunities in combining AI with formal methods and mathematical logic.