The readings shared in Bluesky on 14 May 2026 are:

• An Arrow-theoretic impossibility theorem for the ordinal MVP aggregation problem. ~ Arjun Trivedi. #LeanProver #ITP
• Formal conjectures: An open and evolving benchmark for verified discovery in mathematics. ~ Moritz Firsching et als. #AI4Math #LeanProver
• Formalizing the prime-field Singer construction and Sidon set infrastructure in Lean 4. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz. #LeanProver #ITP #Math
• LeanSearch v2: Global premise retrieval for Lean 4 theorem proving. ~ Guoxiong Gao et als. #AI4Math #LeanProver
• New mathematical workflows. ~ Terence Tao. #AI4Math
• Alon’s Combinatorial Nullstellensatz (in Isabelle/HOL). ~ Arthur Freitas Ramos, Ruy Jose Guerra Barretto de Queiroz, David Barros Hulak. #IsabelleHOL #ITP #Math
• Generalization of Church-Rosser strategies for confluent abstract rewriting systems of the smallest uncountable cardinality. ~ Ievgen Ivanov. #IsabelleHOL #ITP
• The Mostowski collapse theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Verified tableaux: from modal logics to modal fixpoint logics. #CoqProver #ITP #Logic
• Sweep: SWI-Prolog embedded in Emacs. #Prolog #LogicProgramming #Emacs
• Automated conjecturing in mathematics with TxGraffiti. ~ Randy Davila. #AI4Math
• Three cultures of math. ~ Rado Kirov. #Math #AI #AI4Math
• What does AI do for the working mathematician? ~ Krystal Guo. #AI4Math
• #RetoLean4: La sucesión aₙ = 1/n converge a 0. #LeanProver #Math
• #RetoLean4: Retos matemáticos con Lean 4. #LeanProver #Math
• #Vestigium: Reseña de «What does AI do for the working mathematician?». #AI4Math
• #Vestigium: Tres culturas matemáticas ante el avance de la IA. #Math #AI #AI4Math