最近我想明白了一个之前一直没有仔细思考过的关于双生子佯谬的一个问题。

双生子佯谬是狭义相对论里很有名的一个佯谬，它当然早已经很好地被讨论过了，这里先重新叙述一下。

假设地球上有一对双胞胎，一个叫小蓝，一个叫小绫，他们俩的寿命打出生开始就是相等的（废话）。那么，小绫以的速度飞向3光年外的星星，然后到了马上返回，而小蓝留在地球上。在小蓝的视角下，小绫来回这一趟需要的时间是年。而根据狭义相对论的钟慢效应，在小蓝看来，小绫的时钟应该会变慢，系数是倍。也就是小绫的旅程应该经过了8年时间。小绫返回地球的时候，应该比小蓝年轻2岁。

但是如果从小绫的视角，小蓝同样是离开了3光年再返回。钟慢是相对的，小蓝眼中的小绫变慢了，小绫眼中的小蓝也变慢了。整个过程应该是对称的，那就应该是小蓝更年轻...吗？双生子佯谬的正确解释是这个过程是不对称的。虽然速度是相对的，但是加速度是绝对的，小绫到达目的地之后的减速再加速过程使得小绫并不在一个惯性系里，这产生了根本的不对称。也就是说，这件事情实际上涉及到静止、去程、返程三个参考系而不是小蓝、小绫两个参考系。所以“小绫过了8年而小蓝过了6.4年”的观点是错的。实际情况就是小绫比小蓝年轻。

我的问题是这样的。既然钟慢确实是对称的，那么在小蓝的视角，去程花了自己的5年和小绫的4年，返程也花了自己的5年和小绫的4年。但是在小绫的视角，自己花了4年时间到达目的地的星球，小蓝应该只经过了3.2年。返程也是同样，自己4年和小蓝的3.2年。那么剩下的3.6年哪去了呢？

“总不会是在小绫转向那一刻，就花掉了小蓝的3.6年时间吧？”我之前确实是有过这种错误想法的。正确的观点是什么呢？读者不妨先思考一下。

如果要给一个提示的话，“思考这样一个问题，小绫到达目的地的星球的时候，小蓝正在地球上做什么呢？”

本文已同步发布至b站专栏：链接

但是由于b站专栏无法很好地显示注音，推荐在这里阅读www

• 写在前面的话
• 正文
• 后记

写在前面的话

本文是《魔禁》《超炮》和《事象的宏图》的三次创作。虽然但是，没看过《事象的宏图》也可以阅读，所有相关的设定在本文中已经都写出来了。涉及到的cp是海原穹乃×初春饰利（不仅是角色意义上的，也是超能力意义上的）。（想看初春的超能力是怎么用在战斗上的吗！欢迎观看.jpg）

这道题原本是一道旧题：平均要取多少个(0,1)中的随机数才能让和超过1。直接计算期望并不是很困难，就是。我拿到nulladev之后叶子切给了一个新的思路。

设代表距离1还剩x时平均需要的次数，那问题就转化为求。有两部分，一部分是有的概率直接完成，另一部分是取到了小于x的值，比如是t，那剩下的次数还要。也就是说可以列出方程：

化简一下可得：

设，则：

解得，，。

Confounding calender是一个每天一个小解谜游戏小型活动，是大众投稿的。觉得挺有意思，这里跟进一下做一点谜题的推理。

第一天的内容是这样的：

给了你一个12月的日历，有一个持续4天的事件，两个持续3天的事件，三个持续2天的事件，和四个持续1天的事件需要安排。每两个事件之间至少要休息一天，以及9日和26日已经固定了必须是休息日。每行和每列后面的数字是该行有事件的日子之和。这就是一个小纸笔谜题，挺有趣的，可以纯粹逻辑推理解出。

新坑笔记，p-adic数

• 基本概念
• 度量
• 上的所有度量
• 非阿基米德度量

基本概念

在一个集合上的度量是一个集合X到非负实数上的二元函数，满足以下三个条件：

1. ,
2. ,
3. .

附加了度量的集合叫做度量空间。我们要考虑的基本上是域：有加法和乘法，加法成交换群，非零元素对乘法成交换群，以及分配律成立。例如与。在域上，另一个相关的概念是范数，范数是一个域F到非负实数上的一元函数，满足：

1. ,
2. ,
3. .

一个范数可以导出一个度量：。域上的范数的一个例子是上的函数。其导出的度量则是通常意义上的距离。

度量

通常意义上的距离是一种度量，那么上还有没有其他度量呢？

令是任一素数。对于非零整数，定义为能整除的的最高幂次，也就是使得的最大的。例如。约定。

对于任一有理数，定义。定义上的函数如下：

可证得是一范数。事实上，这个范数满足比三角不等式更强的条件。

若范数满足，则称作非阿基米德范数。对于度量，非阿基米德度量为满足的度量。普通的绝对值范数则是阿基米德的。

最近苹果拍的美剧《基地》在Apple TV+上放映了，9月24日放出了前2集，之后每周五一集，仅对Apple TV+付费会员开放。我在预告片放出时关注到了，虽然对苹果的改编感觉很不舒服，但是还是第一时间观看了。下面的总结涉及剧透（显然），斟酌观看。

在预告片中，我们能看出一些大体的剧情线：叙事从谢顿等人被放逐前，盖尔·多尼克加入谢顿计划开始，讲述了一些帝国与谢顿的矛盾，而后至少覆盖塞佛·哈定的剧情部分。但我们可以发现，盖尔·多尼克、塞佛·哈定被改成了女性，帝国皇帝则由Brother Dusk（黄昏兄弟）、Brother Day（白昼兄弟）、Brother Dawn（黎明兄弟）代替。帝国的宰相伊图·丹莫刺尔也被改成了女性机器人。

一时兴起，想尝试翻译一下《Theorem Proving in Lean》。Lean是一个计算机辅助进行数学证明的语言，我接触到了就觉得十分有意思。初学者十分推荐先游玩自然数游戏（虽然没翻译）。本文是Lean语言的入门教程。

• 引言
  • 计算机与定理证明
  • 关于Lean
  • 关于本书
  • 鸣谢

引言

计算机与定理证明

形式化验证是一种使用逻辑推理和计算，去推导用精准的数学术语表达的断言的方法。他们可能包括通常的数学定理，也可能并非通常的数学定理，例如声称一块硬件、一份软件、一条网络协议、或是机械系统、混合系统等等的系统满足所需的标准。在实践上，验证一条数学定理和验证系统的正确性之间并没有很尖锐的分隔线——形式化验证需要使用数学术语描述硬件与软件系统，验证它们的正确性在形式上就可以归结为证明一条定理。相反，证明一条数学定理可能需要冗长的计算，验证证明的正确性就需要验证这一计算过程是否做了它应该做的：也就是系统的正确性。

而支持一条断言的黄金法则就是提供一份证明。20世纪以来逻辑学的发展表明，大部分——如果不是全部——传统的证明方法可以被归结为在任何一个形式体系下很少的几条公理与法则。那么，计算机想要在这里辅助，就有两种方法：一是干脆用计算机来寻找定理的证明方式，二是用计算机帮助验证一个所谓的“证明”是否正确。

自动定理证明就专注于“寻找”这一方面。诸如消解式定理证明、tableau定理证明、快速可满足性求解器等等的工具为我们提供了使用命题逻辑和一阶逻辑来证明公式的方法。其他也有许多系统提供了在特定语言或领域内搜索或是决策的流程，例如整数上或是实数上的线性或非线性表达式。像SMT（satisfiability modulo theories，可满足性模理论）一样的架构，结合了通用领域的搜索方法与专用领域的流程。计算机代数系统和特化的数学软件包也为数学计算、建立上下界、或是寻找数学对象提供了工具。当然，数学计算也可以被视为证明的一种，而上面所说的系统，也同样可以帮助建立数学证明。

自动推理系统则争取的是能力与效率，而通常忽略了严谨性。这样的系统可能出错，也很难保证它们的结果是正确的。另一方面，交互式定理证明则专注于“验证”这一方面。它要求每一句断言都伴随着一个正确的、由公理支持的证明。这就给证明设定了很高的标准：每一条推理和每一步计算都要有之前所建立的定义或是定理的支持，直到最基本的公理和规则。事实上，大部分这样的系统都提供了充分建立好的“证明对象”，以建立系统与系统之间的联系，保证不同的系统之间可以独立地检查正确性。通常，建立这样的证明需要用户输入和交互更多的信息，但是它也让我们可以建立更深也更复杂的证明过程。

Lean Theorem Prover的目标则是填补交互性定理证明与自动化定理证明之间的空白。Lean在框架下，提供了一定程度上自动化的工具和方法，来支持用户的交互以及严谨的公理化证明。它的目标是同时支持数学上的推理，以及复杂系统的推理，在这两个领域都可以验证证明的正确性。

Lean的底层逻辑包含计算性的解释，它可以被看做一种编程语言。也就是说，它可以被看做一个使用精确语义来编写程序的系统，同样也是使用程序计算过程中的函数来推理。Lean也有一套机制使得它可以进行它自己的元编程，也就是说可以使用Lean扩展它自己的功能，实施自动化。在Lean中编程则是另一套与本书配套的教程，在那里会有对元编程更详细的说明，虽然这个系统中一部分计算方面的内容在本书中也会出现。

关于Lean

Lean计划最早由Leonardo de Moura于2013年在Microsoft Research Redmond发起。这是个长程的、进行中的企划，而且其自动化的潜能只能慢慢地被大家所理解。Lean是在Apache 2.0开源协议下发布的。也就是说，它允许其他人自由地使用和拓展Lean的源码以及数学库。

目前，使用Lean有两种方式。第一种是使用Lean在线编辑器。在使用它的时候，你的浏览器会自动下载一个Javascript版本的Lean，一个包含定义和定理的标准库，以及一个编辑器。这提供了一个方便的快速上手的机会。

第二个方式则是将Lean安装到你的电脑上运行。这比在线版要快上许多，而且也更灵活。Visual Studio Code（简称VS Code）和Emacs里的特殊模式为书写和调试证明提供了强有力的帮助，也就更适合严肃的用途。Lean的源码和安装指南可以从这里获取。

本教程描述的是当前版本的Lean，也就是Lean 3。一个老版本Lean 2，对同伦类型论（HoTT）有着特殊支持。在这里你可以找到Lean 2和HoTT库。Lean 2的教程则在这里。

作者：博主与小石。

定义 1. 抛物线规
给定点A与点B，可做以点A为焦点，点B为准点（准点即：抛物线准线与对称轴交点）的抛物线p。

本文探讨使用抛物线规这一工具，以及给定 “可作两抛物线的全部交点” 这一前提，能做到哪些事情。

作图 2. 给定两点A与B，可作两点中点。
以A为焦点以B为准点做抛物线p1，再以B为焦点以A为准点做抛物线p2，易证p1与p2的唯一交点即为A与B的中点。

“以A为焦点以B为准点做抛物线p”之后将被简称为“对A与B做抛物线p”。

作图 3. 给定两点A与B，可作C与D使得四边形ACBD为正方形。
作AB中点M，对M与A做抛物线p1，对M与B做抛物线p2，p1与p2的两个交点C和D满足题意。

已知对角两点作正方形可轻松转化为已知一条边作正方形。

作图 4. 给定两点A与B，可作C与D使得四边形ABDC为正方形。
对AB两点应用作图3作正方形AEBF，再作正方形AMFG与正方形BHFM，再作正方形GMHI，再作正方形GFIC与正方形HDIF，点C与D即为所求。

有了正方形工具与中点工具后，可将线段延长至倍，其中与为任意整数。而且，有正方形工具后，我们可以做出强大的工具：平行四边形工具。

作图 5. 给定三点A、B与C，可作D使得四边形ABCD为平行四边形。
以B与C为对角两点作正方形BECX，再以AE为边作正方形AEFY，再以CF为边作正方形CFGD，点D即为所求。

现在开始，我们考虑以已知两点出发的作图可能。我们将会看到，从已知两点出发，抛物线规强于尺规作图。我们建立坐标系，令已知两点为与。

定义 6. 可作数
a称为可作数，若从与两点出发，可作点。记为。

最近寿美菜子开了youtube频道寿美菜子の〜マジ寿!〜，之后Sphere也开了youtube频道スフィアの 4 colors LABO，感觉Music Ray'n转型了真好啊。怎么说呢，我去过几次Sphere的oneman再加上北京的见面会，感觉和Sphere的距离拉近了一些，一开通youtube就瞬间感觉距离又近了许多。

爱生前段时间也开了一个推特账号，投稿这段居家时间自己画的画（我马上挑了一张夏色奇迹的环凛子的图换了qq头像.jpg）。

#とよさきあき　#おうちでえがこう pic.twitter.com/nIF6SC8bet

— とよさきあき｜お絵かきアカウント【公式】 (@a_toyosaki_yoda) April 29, 2020

我是很喜欢夏色奇迹这部动画，但是人气并不太高，之前还想过，会不会被Sphere忘了什么的。但是果然声优们是会记得的，就像她在京阿尼事件之后的广播中说的一样，制作人和声优一定是对作品有着满满的爱，才会制作出这么好的能让观众都喜欢的作品来。爱生肯定也是，轻音还是夏色还是前天画的《初恋的绘本》的美桜。真好啊。

编程中遇到的一个问题。在python里重定向所有的如print等的结果并不困难，只需要给sys.stdout赋值一个文件对象即可（实际上在python3.4及以后，contextlib里就有一个redirect_stdout的函数可以直接运行）。

（翻译自https://eli.thegreenplace.net/2015/redirecting-all-kinds-of-stdout-in-python/）

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

import sys
from contextlib import contextmanager

@contextmanager
def redirect_stdout(stream):
    old_stdout = sys.stdout
    sys.stdout = stream
    try：
        yield
    finally:
        sys.stdout = old_stdout

f = io.StringIO()
with redirect_stdout(f):
    print('foobar')
    print(12)
print('Got stdout: "{0}"'.format(f.getvalue()))

但是，如果某个module里有在C里直接printf或是cout字符串，上面的就不管用了。比如例子：

1
2
3
4
5
6
7
8
9
10

import ctypes
libc = ctypes.CDLL(None)

f = io.StringIO()
with stdout_redirector(f):
    print('foobar')
    print(12)
    libc.puts(b'this comes from C')
    os.system('echo and this is from echo')
print('Got stdout: "{0}"'.format(f.getvalue()))

使用ctypes模拟C中的puts函数，这和在Python中调用C的函数输出到stdout的结果是一样的。另一个测试是使用os.system创建一个子进程同样输出至stdout。而这的运行结果是：

1
2
3
4
5

this comes from C
and this is from echo
Got stdout: "foobar
12
"

print的结果相同，而puts和echo则直接跳过了重定向被输出到了屏幕上。这是为什么呢？