Welcome to Import AI, a newsletter about AI research. Import AI runs on arXiv and feedback from readers. If you’d like to support this, please subscribe. Subscribe now The era of math proof automation has arrived:…Numina-Lean-Agent shows how math will never be the same…In the past few years, large-scale AI models have become good at…

Import AI 

AI systems are achieving breakthrough capabilities in mathematical proof automation, with Numina-Lean-Agent solving all Putnam 2025 problems using general foundation models. Cybersecurity faces industrialization as LLMs like Opus 4.5 and GPT-5.2 successfully generate exploits for zero-day vulnerabilities, suggesting offensive cyber operations will soon scale with token throughput rather than human hackers. Economic analysis indicates AI could be the most transformative technology ever, potentially warranting 5-10% of GDP investment in safety measures given existential risks. Labor market research shows 26.5 million highly AI-exposed workers have strong adaptive capacity for job transitions, though 6.1 million in clerical roles face significant displacement risk with limited transferability options.

Import AI 442: Winners and losers in the AI economy; math proof automation; and industrialization of cyber espionage