The readings shared in Bluesky on 19 April 2026 are:

• A quadratic form generalization of rational dinv. ~ Yifeng Huang. #LeanProver #ITP #AI4Math
• Automated tactics for polynomial reasoning in Lean 4. ~ Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math
• Automated tactics for polynomial reasoning in Lean 4. ~ Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math
• Formalizing Wu-Ritt method in Lean 4. ~ Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, Lihong Zhi. #LeanProver #ITP #AI4Math
• Lean: How AI and proof automation are changing mathematics. ~ Leonardo de Moura. #LeanProver #ITP #AI4Math
• On the formalization of IUT (inter-universal Teichmüller theory): a preliminary progress report. ~ Shinichi Mochizuki. #LeanProver #ITP #Maht
• Teaching mathematics using Verbose Lean. ~ Patrick Massot. #LeanProver #ITP #Math
• Teaching with Lean for supporting the transition to university mathematics. ~ Paola Iannone. #LeanProver #ITP #Math
• What goes into formalizing Fermat?. ~ Kevin Buzzard. #LeanProver #ITP #Math
• A proof engineering perspective on formalising combinatorics in Isabelle/HOL. ~ Chelsea Edmonds. #IsabelleHOL #ITP #AI4Math
• Automated conjecture resolution with formal verification. ~ Haocheng Ju et als. #AI4Math #LeanProver #ITP
• Beyond QED: AI, theorem proving, and the quest for beautiful proofs. ~ Natarajan Shankar. #AI4Math #ITP
• PKU AI disproves Anderson conjecture: China's first autonomous math breakthrough. ~ Sophia Langford. #AI4Math #LeanProver
• Una IA china resuelve en 80 horas un problema matemático atascado hace doce años. ~ Pau Roldan. #AI4Math #LeanProver #ITP
• The agentification of scientific research: A physicist's perspective. ~ Xiao-Liang Qi. #AI4Science
• Reseña de «Automated conjecture resolution with formal verification». #AI4Math #LeanProver #ITP