一种类别的宇宙

主要观点:2024 年作者在多个领域学习和实践,包括从爱丁堡搬到剑桥、研究 Lean 定理证明器的决策程序、学习 SAT 求解及相关理论、编写 SAT 求解器、接触其他决策程序、参与剑桥的课程和项目、学习摄影和音乐、研读莎士比亚和诗歌等,对未来一年也有诸多计划。
关键信息

  • 研究小组迁移,确定 PhD 研究方向为设计、实现和验证 Lean 定理证明器的决策程序。
  • 与朋友讨论学习 SAT 求解及 UNSAT 证明相关理论,如 Resolution 等。
  • 实现 SAT 求解器并撰写其正确性证明。
  • 接触多种决策程序,如 Tarski 量词消除等。
  • 参加剑桥的课程如描述复杂性、指称语义等。
  • 指导学生进行相关项目,如实现组合递归等式的决策程序等。
  • 学习摄影,通过写射线追踪模拟理解光学现象,阅读暗表用户手册。
  • 重新开始弹钢琴,学习作曲理论,如对位法等。
  • 正式验证追踪器 Monodrone,扩展其和弦识别算法。
  • 参加莎士比亚相关活动,开始喜欢莎士比亚作品。
  • 收集喜欢的诗歌,计划明年继续阅读史诗诗歌。
  • 有明年的学习和实践计划,如实现决策程序、学习数域课程等。
    重要细节
  • 阅读 Bitwuzla 源代码用于 Lean 中的形式验证。
  • 参考课程如 Little Engines of Proof 了解部分决策程序。
  • 用 egui 写代码,喜欢其 API 更 ergonomic。
  • 观看 Glenn Gould 的视频,了解其对音乐的观点。
  • 因 AWS 需求与验证追踪器相关的工作。
  • 对现代主义诗歌的看法及喜欢的诗人作品。
  • 阅读多种书籍,如关于 Shinto 神社等。
  • 计划明年的具体学习和实践内容及目标。
阅读 5
0 条评论