『Iowa Type Theory Commute』のカバーアート

Iowa Type Theory Commute

Iowa Type Theory Commute

著者： Aaron Stump
無料で聴く

【Amazonプライム会員限定】今ならプレミアムプランが4か月 月額99円。

10月19日まで。※適用条件あり
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.© 2026 Iowa Type Theory Commute 数学 科学
エピソード
  • Autoformalization of Fermat's Last Theorem

    Autoformalization of Fermat's Last Theorem
    2026/09/15

    In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the proof of Fermat's Last Theorem. That is, they instructed an LLM to create a computer-checkable proof, in the Lean prover, of this theorem, following existing paper proofs in the literature. The resulting proof weighs in at 13 million lines of Lean, a staggering amount.
    続きを読む 一部表示
    14 分
  • A Fireball of Alpha

    A Fireball of Alpha
    2026/08/21

    I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church. One reason to do that, besides just a love of being ornery, is to be able to state and prove theorems about alpha-equivalence. One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables. I have a companion blog post that talks about this, with a link to the repo with my Agda code so far.
    続きを読む 一部表示
    20 分
  • Solving Quadratic Word Equations

    Solving Quadratic Word Equations
    2026/08/11

    A system of word equations is called quadratic if no variable occurs more than twice in it. There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode. My source is Chapter 12 of "Algebraic Combinatorics on Words" by Lothaire.
    続きを読む 一部表示
    23 分
adbl_web_anon_alc_button_suppression_t1
まだレビューはありません