The readings shared in Mastodon on 5 October 2024 are

• Readings shared October 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Python
• ENS-Lean-course: Taxicab number in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Sets in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Homework 3: Sets. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• PCC116-2021: Lógica aplicada à computação (2021/22). ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Agda #Logic #Math #CompSci
• PCC116: Lógica aplicada à computação (2024). ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #CompSci
• PCC116: Aula 1: Lógica proposicional em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math
• PCC116: Aula 2: Predicate logic in Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math
• PCC116: Aula 3: Programação funcional em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 4: Programação funcional e recursividade em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 5: Listas encadeadas (tipo List na biblioteca) em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 6: Predicados indutivos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 8: Programando com tipos dependentes em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 9: Sobrecarga e classes de tipos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 10: Metaprogramação e automação de provas em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 11: Recursão geral em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 12: Representando semântica formal em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 13: λ-cálculo tipado simples em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 14: Formalizando em Lean compiladores / semântica de linguagens imperativas. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 15: Modelagem de autômatos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• Terence Tao’s vision of AI assistants in research mathematics. ~ David H Bailey. #Math #AI #ITP #LeanProver