The readings shared in Bluesky on 22 October 2025 are:

• Formal or not formal? That is the question in AI for theorem proving. ~ Kevin Buzzard. #AI #Math #LLM #ITP #LeanProver
• Formalisation of the Calderón transference principle in ergodic theory. ~ Felix Pernegger. #ITP #LeanProver #Math
• OpenAI researcher forced to delete “embarrassing” tweet claiming huge breakthrough. ~ Frank Landymore. #AI #Math
• Leading OpenAI researcher announced a GPT-5 math breakthrough that never happened. ~ Matthias Bastian. #AI #Math
• PhysLean: A talk for physics undergraduates. ~ Joseph Tooby-Smith. #ITP #LeanProver #Math #Physics
• Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof. ~ Boris Alexeev, ChatGPT, Lean, Dustin G. Mixon. #AI #Math #LLM #ChatGPT #ITP #LeanProver
• Una refutación inusual del problema de Erdős #707: Colaboración humano-IA y el papel de Lean. #AI #Math #LLM #ITP #LeanProver
• #Exercitium: Elementos no repetidos. #Haskell #ProgramaciónFuncional #Matemáticas