著名的科学家曾经说过： 这难道是一道题吗？？
按照目前的粒子物理标准模型，共有六种夸克，按质量从小到大分为三代，各代的性质也有所不同。
(i) 目前的标准模型里，描述三代夸克间通过W粒子弱相互作用的耦合强度的三阶矩阵为：
下列有关此矩阵以及夸克的描述中错误的是：
由于微博常年不用，文章挂了，这里补档一下2017年我和yui第一次去日本的时候我写的游记。
食用须知：由于我不喜欢图太多的游记所以这里图会比较少。。。另外这游记不能当攻略看，因为我不会写“如何获取信息”的过程，我只是想记录一下而已（观赏用，嗯）估计看的人不会太多吧。另外，我是以我的视角写的，所以我和yui分开的时间段里yui干的事情我就没怎么写。而且，我本身不大喜欢看图特别多的文章，所以虽然我拍了300多上照片，但是这游记里图多的地方就一块。。。
这次旅游本来从去年就开始准备了。本来是预计我和yui寒假去的，结果因为我考研、做游戏，yui考期末等各种事情，开始准备的时间玩了，最后没来得及签证，没去成。
于是转战了今年暑假，成了我的毕业旅行。大概在上学的时候，我最先得知了sphere的live在8月12大阪和8月13东京两场，之后查询了在那段时间附近的活动，有c92，aqours live和poppin party live，刚好规划在11~21日的话，能赶上CM和3场live。
后来，在我学校的lovelive群里，我又遇见了两个一起去水团live的同学，暂且成为lolo和kokoro。于是我们4个人一起开始拟定行程，并定下了8月10~14日在东京，之后去箱根和沼津，16日到大阪与京都，21日再回东京的大致行程。
途中发生过一件事。在我想起来买sphere live的门票的时候，刚好晚了几天，eplus上已经卖光了。在我去ticketcamp看的时候，见到了一张要去便利店取的挺便宜的票。在这里我特别感谢砂粑粑，当时在我印象中认识的在日本的只有砂和冰月，我拜托砂帮我在tc上买并去便利店取票这么麻烦的事，砂也帮我买到了票并邮了过来，真的是十分感谢！虽然现在看来，当时那张暗票是约10000yen拿到了二阶山顶票，不如现在（写这篇游记的时间）在tc上的一阶中后排15000，但是毕竟是第一次，没有经验。以后应该会更有经验的。
在这之后，在我们拟购买机票和民宿的时候，在我这儿出了点问题。同学们都说日本签证很好过，想赶快购买机票与民宿防止涨价，但是由于我手里没有足够的钱，家长又怕拒签损失，让我先办签证之后再机宿，lolo和kokoro只好先订了他们俩那份。加之在拟定行程时发现，我和yui很多一起要去的地方（比如东方、轻音相关）他俩兴趣不大，他俩又有很多地方我们兴趣不大，最后我们选择了分开行动。
之后，我和yui便加紧开始准备签证，选择机宿，并细化行程单。现在我俩定下的行程单大致是：8月10日下午抵达东京，在住处秋叶原附近买c92的catalog和kbx（因为sphere场贩没有官棒）；11日早起去c92，晚上去晴空塔；12日去东京迪士尼；13日去明治神宫、涩谷新宿附近，晚上我去中野看sphere的live；14日去浅草寺上野公园皇居附近，晚上去箱根住；15日在沼津LLSS巡礼；16日去大阪，下午去京都的伏见稻荷；17日先去奈良看春日神社东大寺，下午回大阪去大阪城；18日先去丰乡巡礼轻音，下午回京都去京阿尼shop附近；19日去京都吧剩下的看了，八坂神社清水寺二条城金阁寺天满宫；20日上午空出半天去京都未定，晚上回东京看花火大会；21日在秋叶原附近LL巡礼，下午去银座，晚上我去看邦邦live；22日在秋叶原附近收尾之后晚上做飞机回来。
另外，在我说要去c92之后，有好多人让我去c92代购了一大堆东西。。。一开始是yuki想要天空璋作为rep楼奖品（结果因为zun限购，只能买通贩了），之后几个熟人又给我列了几个清单，我还赞助了一个代购作为rep楼奖品。。。总觉得包要撑爆
额外提一句，看sphere的call表的时候发现sphere的振付好多。。。
之后再准备好必要的东西之后，明天我们就要出发了！
最近我想明白了一个之前一直没有仔细思考过的关于双生子佯谬的一个问题。
双生子佯谬是狭义相对论里很有名的一个佯谬，它当然早已经很好地被讨论过了，这里先重新叙述一下。
假设地球上有一对双胞胎，一个叫小蓝，一个叫小绫，他们俩的寿命打出生开始就是相等的（废话）。那么，小绫以
但是如果从小绫的视角，小蓝同样是离开了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。直接计算期望并不是很困难，就是
设
化简一下可得：
设
解得
Confounding calender是一个每天一个小解谜游戏小型活动，是大众投稿的。觉得挺有意思，这里跟进一下做一点谜题的推理。
第一天的内容是这样的：
给了你一个12月的日历，有一个持续4天的事件，两个持续3天的事件，三个持续2天的事件，和四个持续1天的事件需要安排。每两个事件之间至少要休息一天，以及9日和26日已经固定了必须是休息日。每行和每列后面的数字是该行有事件的日子之和。这就是一个小纸笔谜题，挺有趣的，可以纯粹逻辑推理解出。
新坑笔记，p-adic数
在一个集合上的度量是一个集合X到非负实数上的二元函数
附加了度量的集合叫做度量空间。我们要考虑的基本上是域：有加法和乘法，加法成交换群，非零元素对乘法成交换群，以及分配律成立。例如
一个范数可以导出一个度量：
通常意义上的距离是一种度量，那么
令
对于任一有理数
可证得
若范数满足
最近苹果拍的美剧《基地》在Apple TV+上放映了，9月24日放出了前2集，之后每周五一集，仅对Apple TV+付费会员开放。我在预告片放出时关注到了，虽然对苹果的改编感觉很不舒服，但是还是第一时间观看了。下面的总结涉及剧透（显然），斟酌观看。
在预告片中，我们能看出一些大体的剧情线：叙事从谢顿等人被放逐前，盖尔·多尼克加入谢顿计划开始，讲述了一些帝国与谢顿的矛盾，而后至少覆盖塞佛·哈定的剧情部分。但我们可以发现，盖尔·多尼克、塞佛·哈定被改成了女性，帝国皇帝则由Brother Dusk（黄昏兄弟）、Brother Day（白昼兄弟）、Brother Dawn（黎明兄弟）代替。帝国的宰相伊图·丹莫刺尔也被改成了女性机器人。
一时兴起，想尝试翻译一下《Theorem Proving in Lean》。Lean是一个计算机辅助进行数学证明的语言，我接触到了就觉得十分有意思。初学者十分推荐先游玩自然数游戏（虽然没翻译）。本文是Lean语言的入门教程。
形式化验证是一种使用逻辑推理和计算，去推导用精准的数学术语表达的断言的方法。他们可能包括通常的数学定理，也可能并非通常的数学定理，例如声称一块硬件、一份软件、一条网络协议、或是机械系统、混合系统等等的系统满足所需的标准。在实践上，验证一条数学定理和验证系统的正确性之间并没有很尖锐的分隔线——形式化验证需要使用数学术语描述硬件与软件系统，验证它们的正确性在形式上就可以归结为证明一条定理。相反，证明一条数学定理可能需要冗长的计算，验证证明的正确性就需要验证这一计算过程是否做了它应该做的：也就是系统的正确性。
而支持一条断言的黄金法则就是提供一份证明。20世纪以来逻辑学的发展表明，大部分——如果不是全部——传统的证明方法可以被归结为在任何一个形式体系下很少的几条公理与法则。那么，计算机想要在这里辅助，就有两种方法：一是干脆用计算机来寻找定理的证明方式，二是用计算机帮助验证一个所谓的“证明”是否正确。
自动定理证明就专注于“寻找”这一方面。诸如消解式定理证明、tableau定理证明、快速可满足性求解器等等的工具为我们提供了使用命题逻辑和一阶逻辑来证明公式的方法。其他也有许多系统提供了在特定语言或领域内搜索或是决策的流程，例如整数上或是实数上的线性或非线性表达式。像SMT（satisfiability modulo theories，可满足性模理论）一样的架构，结合了通用领域的搜索方法与专用领域的流程。计算机代数系统和特化的数学软件包也为数学计算、建立上下界、或是寻找数学对象提供了工具。当然，数学计算也可以被视为证明的一种，而上面所说的系统，也同样可以帮助建立数学证明。
自动推理系统则争取的是能力与效率，而通常忽略了严谨性。这样的系统可能出错，也很难保证它们的结果是正确的。另一方面，交互式定理证明则专注于“验证”这一方面。它要求每一句断言都伴随着一个正确的、由公理支持的证明。这就给证明设定了很高的标准：每一条推理和每一步计算都要有之前所建立的定义或是定理的支持，直到最基本的公理和规则。事实上，大部分这样的系统都提供了充分建立好的“证明对象”，以建立系统与系统之间的联系，保证不同的系统之间可以独立地检查正确性。通常，建立这样的证明需要用户输入和交互更多的信息，但是它也让我们可以建立更深也更复杂的证明过程。
Lean Theorem Prover的目标则是填补交互性定理证明与自动化定理证明之间的空白。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称为可作数，若从
