在 X Round 4 上做到了「尺规作图」这道非常有意思的提交答案题，后来得知这题的灵感来自于 Euclidea 这款智力游戏，于是决定体验一下。
然后就意识到自己的几何水平退化实在太厉害了…于是决定写篇博客来记录一下自己解题的心路历程。
继续阅读Euclidea 游戏解答与证明归纳证明方法论——使用归纳法构建一般性结论的证明
（本文是对 James Wilcox 的 Exercises on Generalizing the Induction Hypothesis 的一点详细解说，也感谢 James Wilcox 在文章中提供的几道颇有练习价值的证明题！）
由于大多数数据类型常见的递归属性，在 Coq 中使用归纳法证明命题是一件颇为常见且基础的操作。
然而，有些具有递归性质的命题并不易于使用归纳法直接进行证明，原因在于，这些命题中的部分变量取了特定的值，而归纳过程中这些变量的值会发生变化，从而导致归纳过程无法继续下去。对此，我们往往需要找到一个更一般性的命题，用归纳法证明这一一般命题，随后使用该一般命题构建对原命题的证明。
下面便是两道实践此类命题证明方法论的绝佳例题。
继续阅读归纳证明方法论——使用归纳法构建一般性结论的证明2023 上半年总结
充实，还是空耗
其实现在写这篇总结似乎还为时过早，因为上半年的事情还不能说全部处理完毕，还有多达 4 学分，两门课程的作业没有全部完成。这两门课又全是同一个陌生领域，理论计算机科学的硬课，未知性带来的心理负担可想而知。
总觉得每挺过一个 ddl，压力应该会递减，结果这学期的经历直接啪啪打脸。因为每翻过一个 ddl，才发现接下来的水相比更深了一些。虽然早有心理准备，但心理准备和真正面对还是两回事。
继续阅读2023 上半年总结MIT 18.408 概率可验证证明 学习笔记 一 – 基本概念
APIO 2023 游记（大雾）
Day 0
去程没订到动集的票，于是只好进行一个中转。订了京扬直特 Z29 次，然后再走宁启铁路到南京。
感谢这趟车让我知道了“明光”这个地名。看得出来当地为了能停几趟进京直特和桶，下了血本啊（）
这应该是我第一次来到北京站了。作为当年北京十大建筑之一，北京站无论从外观还是内部装修，都能感受到一种较为庄重的氛围。
继续阅读APIO 2023 游记（大雾）MIT 18.408 概率可验证证明 学习笔记 序
本系列是 MIT 18.408 Topics in Theoretical Computer Science: Probabilistically Checkable Proofs Fall 2022 的学习笔记。该课程内容也被用于北京理工大学 2023 春季学期的组合数学课程。
该系列全部内容均采用 CC BY-NC-SA 4.0 协议进行许可。
继续阅读MIT 18.408 概率可验证证明 学习笔记 序ICPC EC Final 2022 游记
Day -1
想着早点到上海，留出点时间随机游走，于是订了足够早出发（十点整）的 G7 次的车票。结果就是不得不八点多出门赶车。
运气不太好，没赶上早高峰房山线跨线进 9 号线的车，换乘次数 +1。
到北京南站的时候离开车差不多半个小时，过了安检上楼之后刚好赶上开始检票，冗余时间感觉不太充足。
上车的人是真的多，怪不得京沪高铁能赚钱（）
订的票很不幸地是 01 排，结果就是面前没有座位了，对于我们这样的三人连座来说，由于过道在车厢中间位置，桌板的大小缩了不少，坐在靠过道的我为了用上桌板还得往窗户那边凑过去。
虹桥 2 号航站楼的伪虚拟换乘挺有意思。名义上是虚拟换乘车站，但是可以在中间两个轨道停车的时候通过穿过车厢的方式实现换乘。
在同济的高中好友邀我去看花，然而发现四平路离宝山并不算近，再加上身心颇为疲惫，只得婉拒，颇为遗憾。
晚上我校的几个队（可惜 ddl 不在）找了个上海菜馆恰饭。菜馆是对着 知乎上的一个清单 找的，味道确实不错，很符合我对上海菜的想象！
继续阅读ICPC EC Final 2022 游记2022 下半年总结
失落时间
如果给这学期找一个恰当的关键词，那么“失落”似乎是一个不错的候选。
为何这么描述？看起来过去的这半年我确实取得了一些成绩，但在这些成绩之下，却埋藏着不安，迷茫与彷徨，以及空虚与失焦感。
继续阅读2022 下半年总结谈谈 Windows 与 Linux 双系统环境下的时间不同步问题
在 Windows 和 Linux 两个操作系统间切换时，会产生时间不同步的问题——从 Windows 系统切换到 Linux 系统时，时间会向后推 8 小时；而当从 Linux 系统切换回 Windows 系统的时候，时间又向前推了 8 小时。
继续阅读谈谈 Windows 与 Linux 双系统环境下的时间不同步问题从零开始的 Arch Linux 踩坑纪实
2022 上半年总结
摸鱼学期
虽然学期内每天都在为大物而忧心，不过这学期最后还是有惊无险地结束了。嘛，一部分原因是期末线上考试，改成了全选择题。
现在看来这学期比上学期摸的不是一点两点的厉害（雀力在这半年里大幅提升了），在这样的情况下还能避免在多条战线上的全面溃败也是一大奇迹。