主要观点：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 神社等。
• 计划明年的具体学习和实践内容及目标。