进入七月，京局以汛期的理由停开了京原线小票车 6437/8 次。去年夏天发生在北京西部山区的洪灾至今还令人历历在目：丰沙线三列客车被困于途中，在铁路和地方的协助救援下旅客和乘务员才得以疏散。之后虽然洪水退去，但是对北京西部铁路的影响仍然是长远的：京原线客运中断三月有余，直到入冬才得以重开，丰沙线客运则至今尚未恢复，不少客车只得改道其他路线。
然而，京原沿线仍有不少乘客需要火车出行。为此，京局决定视情况加开临客列车作为 6437/8 次的替代，而由于 6437/8 属于普客，普客并没有像其他列车等级一样划定专用的临客号段，京局只好重新启用多年未用的 L 字头号段开行这些临客列车。而除了京原线，位于北京东北方向的的锦承线也开行了类似的 L 字头列车。这一举动很快传播开来，吸引了不少铁路爱好者的关注。
继续阅读2024 夏 京原线临客运转退役 OIer 文化课交流群（以下简称“退群”）每年都会举办一次被称为“退群杯”的大型活动。前两届是面向文化课选手的文化课竞赛，第三届是 ICPC 赛制的算法竞赛，今年则是一次颇为正式的学术会议，正经到还拥有一个颇为正式的名字，TUIQUN（Tuiqun Universe In Quaint Ultimate Non-summit）。
二月份征稿启示便已经贴出，原本计划在五一黄金周举办线上会议。只可惜因为投稿数量不足，会议并没有如期在五一举行。不过到了九月份，有了些投稿，会议也就变成了现实，形式也从线上会议升级为线下会议。
一开始听到举办地在杭州，我其实并不是很想前去——亚运举办地叠加国庆黄金周，车票难买，人潮汹涌，实在不是一个前往杭州的合适时间点。不过还是决定先赶着放票时间买了去程的车票，思考几天后再作决定。反正提前一周退票是不收取退票费的嘛。
在北京的退群群友其实不少，刚好也有会议的讲者在北京，大家便商量着能否在北京办分会场。仔细一想，如果只是单单听讲者的汇报，呆在北京确实是一个不错的选择。不过学术生活中，线下的社交活动也是很重要的一环，在线下参会，能与讲者及其他听众间进行面对面的交流。交流过程中，不仅仅能在知识层面上获得收获，还能获得在学术方法论上的指引和一些生活方面的经验，这些软收获对于个人未来的发展有着不可忽视的作用。更何况 TUIQUN 相较正式的学术会议而言，本身就具有更浓厚的社交性质，不到现场参会，活动的意义就减损了大半。一番考量后，最后还是下定决心，奔赴杭州的线下主会场。
既然都跑了这么远，那么参加完会议就立刻返回北京就实在不算划算了。就这样，国庆黄金周的沪杭旅行提上了日程。对我来说，长途旅行自然少不了精心策划的铁路运转。虽然我并不太愿意安排完全围绕铁路的运转旅行，但在旅行过程中顺带穿插一些铁路运转的部分倒是正合我的心意。
继续阅读2023 秋 沪杭旅行 & TUIQUN 2023 游记我一个已经退役的 OIer，怎么又去参加 APIO 了呢？
咳咳，事情的起因是这样的：CCF 在 2021 年创办了青少年计算机教育研讨会（Workshop on Computing Education for Teenagers，WCET），在每次线下 OI 活动时会组织面向教师的论坛。由于本次 WCET 活动和 APIO 一块在华山饭店进行，一方面刚好能借此接触到参与 APIO 的选手们，另外一方面也能了解一些算法竞赛与信息技术课程教学动态。对于我这样一位旅游型和社交型选手而言，怎么可能会错失这一面基与交流机会呢？
本来 小花 也想来的，但因为赶大作业推掉了这次行程，于是这次就是我独自一个人去了。
继续阅读APIO 2023 游记（大雾）十二月初突然传来消息，行走于京原线上的非空列车 6437/8 次将要更换空调车底。对于从来没乘坐过非空调列车的我来说，虽然能理解新事物终将取代旧事物的道理，但不可避免地为非空列车的远去而惋惜，也为即将失去的体验机会而遗憾。而 6437/8 次作为离我最近的一趟非空列车，抢救性运转体验也是最容易的。
10 号那天，在丰台机务段参加“毛泽东号”机车研学活动之后，我便来到了北京西站，乘坐了 6437 次列车的北京西-燕山区间。当天是周末，已经有不少学生车迷赶来送别，能看到不少长枪短炮和手机不断地进行拍摄。这一趟坐下来一个多小时，感觉非空列车确实带给了我不少独特的体验，但总感觉体验上还差点意思。
想着 19 号那天来送别的人应该会比较多，也有机会遇到认识的朋友，我就又订了一张 19 号北京-燕山的 6437 次列车的车票（由于想要送别的人和单纯留下车票纪念的人非常多，订票的时候已经只能买到无座车票了，而之后几天再看的时候，就连无座也都不剩了）。在出发的前一夜，越想越觉得该彻底体验下非空列车的我，决定将目的地从燕山延长到涞源，赶着 12306 系统维护的时间到来之前买好了延长段和返程的车票，并订好了涞源过夜的旅馆，这一系列动作进行的非常流畅，完全没有一丝犹豫。
于是这场漫长的送别之旅，就这样开始了。
继续阅读京原线非空列车 6437/8 次告别之旅算下来，距离上一次真正意义上的长途旅行，已经是三年半的时间了。
2018 年的 NOIp，因为种种机缘巧合，拿了个还不算差的成绩，得以前往广州冬眠参加冬令营（WC 2019 游记），运气很好拿了块铜牌。
后来因为种种原因，原来不在省队线内的我意外进了队，于是就有了 CTS 2019 & APIO 2019 的旅行，当然还有更重要的 NOI 2019 啦。遗憾的是这三次比赛都没能拿到奖项，特别是最重要的 NOI 2019，比赛结束之后我的心态也进入了一个低谷期。
2020 年疫情突然降临，首先推掉的就是当年的冬令营。原本大家都认为这一次和 2003 年那样，并不会持续太久时间，到了暑假一切活动都会恢复正常，没想到一晃就是三年。当年的 WC 和 APIO 都在暑假迁移到了线上，而 NOI 2020 最终未能成行，成为我 OI 时光最大的遗憾。
（非常抱歉先用流水帐记了这么多之前提过的往事，有点偏题了 qwq）
转眼间过完了高中三年，大学也已经过去了一年半，长途旅行终于再次成为一个可选项。也因此在春节之后，我开始为这次旅行策划立项，做起规划。
首先估摸了下旅行的时间。因为今年极早的春节+比较晚的开学时间，整个寒假的时长达到了 50 日，如果选择在元宵节后出发，算下来差不多有 10 天的旅行时间，这样充裕的时间，恐怕之后都很难再找到了。
在这一前提下，接下来需要决定的就是旅行的目的地了。在这一问题上，我一开始就定下了广度优先的路线。在一省之内花掉十天时间，固然可以吃透当地大部分的旅游资源，但在人文风情等方面则显得有些单调了。
最终目的地被选定为湖北、湖南、广东三省的中心城市：武汉、长沙、广州及深圳。而因为这条旅游路线大体沿着京广铁路，这次旅行也有了“京广路旅行”的名字。
继续阅读2023 春 京广路旅行（本文是对 James Wilcox 的 Exercises on Generalizing the Induction Hypothesis 的一点详细解说，也感谢 James Wilcox 在文章中提供的几道颇有练习价值的证明题！）
由于大多数数据类型常见的递归属性，在 Coq 中使用归纳法证明命题是一件颇为常见且基础的操作。
然而，有些具有递归性质的命题并不易于使用归纳法直接进行证明，原因在于，这些命题中的部分变量取了特定的值，而归纳过程中这些变量的值会发生变化，从而导致归纳过程无法继续下去。对此，我们往往需要找到一个更一般性的命题，用归纳法证明这一一般命题，随后使用该一般命题构建对原命题的证明。
下面便是两道实践此类命题证明方法论的绝佳例题。
继续阅读归纳证明方法论——使用归纳法构建一般性结论的证明其实现在写这篇总结似乎还为时过早，因为上半年的事情还不能说全部处理完毕，还有多达 4 学分，两门课程的作业没有全部完成。这两门课又全是同一个陌生领域，理论计算机科学的硬课，未知性带来的心理负担可想而知。
总觉得每挺过一个 ddl，压力应该会递减，结果这学期的经历直接啪啪打脸。因为每翻过一个 ddl，才发现接下来的水相比更深了一些。虽然早有心理准备，但心理准备和真正面对还是两回事。
继续阅读2023 上半年总结本系列是 MIT 18.408 Topics in Theoretical Computer Science: Probabilistically Checkable Proofs Fall 2022 的学习笔记。该课程内容也被用于北京理工大学 2023 春季学期的组合数学课程。
该系列全部内容均采用 CC BY-NC-SA 4.0 协议进行许可。
继续阅读MIT 18.408 概率可验证证明 学习笔记 序想着早点到上海，留出点时间随机游走，于是订了足够早出发（十点整）的 G7 次的车票。结果就是不得不八点多出门赶车。
运气不太好，没赶上早高峰房山线跨线进 9 号线的车，换乘次数 +1。
到北京南站的时候离开车差不多半个小时，过了安检上楼之后刚好赶上开始检票，冗余时间感觉不太充足。
上车的人是真的多，怪不得京沪高铁能赚钱（）
订的票很不幸地是 01 排，结果就是面前没有座位了，对于我们这样的三人连座来说，由于过道在车厢中间位置，桌板的大小缩了不少，坐在靠过道的我为了用上桌板还得往窗户那边凑过去。
虹桥 2 号航站楼的伪虚拟换乘挺有意思。名义上是虚拟换乘车站，但是可以在中间两个轨道停车的时候通过穿过车厢的方式实现换乘。
在同济的高中好友邀我去看花，然而发现四平路离宝山并不算近，再加上身心颇为疲惫，只得婉拒，颇为遗憾。
晚上我校的几个队（可惜 ddl 不在）找了个上海菜馆恰饭。菜馆是对着 知乎上的一个清单 找的，味道确实不错，很符合我对上海菜的想象！
继续阅读ICPC EC Final 2022 游记