Johndcook
John D. Cook，数学与计算机科学顾问的博客，分享关于数学、统计、编程与科学计算的文章。
评论
点赞
收藏形式化方法让你探索边缘角落
用高维几何中"球体体积占比趋近于零"的数学现象，解释形式化验证方法的价值——软件功能组合成百上千时，直觉覆盖不到的边缘路径加起来可能占绝大多数运行场景。 文章给出 Python 代码演示维度与体积比的关系，并在末尾指出几何维度与软件功能组合的不完全等价性。
OpenAI的Navier-Stokes证明背后，被忽视的四数量级成本突破
OpenAI发布Navier-Stokes方程证明的同时附上了Lean 4形式化证明。传统形式化证明需40小时/页，而OpenAI仅用17小时完成166页论文的验证，成本降低四个数量级。 形式验证还可应用于安全策略一致性、智能合约、关键算法等领域。
RSA-260 Factored
Eric Lu 成功分解了 RSA-260（260位数字/862比特），这是迄今最大被分解的RSA挑战数。他估算成本约4,900 GPU天，折合约40万美元。 862比特RSA密钥的安全强度仅约74比特，远低于当前推荐的2048比特（107比特安全）。
线性代数的专利应用：一种并行处理器编译器的代数化方法
John D. Cook 与 Brian Beckman 获得了一项关于并行处理器编译器的专利，核心思路是用二元域上的线性代数来形式化位操作。将计算归约为代数运算后，可以证明操作序列的正确性，并通过化简表达式找到优化空间。 他们为此设计了一种叫 Tartan 的编程语言，名称源于矩阵掩码图案类似苏格兰格纹。 
让不必要的事变得更简单
AI教程视频里一堆"用AI监控新闻、用AI点外卖、用AI管理消息"的案例，本质是用技术解决技术制造的问题——让不需要做的事变得更轻松。 作者认为这类用例很多是YouTube博主为了吸引流量编出来的，不是真实需求。真正的生产力自动化高度个人化，自己最有用的脚本对别人毫无价值。
为什么叫"超球面"多项式？
超球面多项式（Gegenbauer多项式）是勒让德多项式的推广，得名于数学家Gegenbauer，因其在超球面上求解拉普拉斯方程时自然出现而得名"超球面"。 "超球面"并非指"极其球面"，而是指"超越三维球面"——在n>3维空间中求解拉普拉斯方程时自然出现。现代术语更倾向用hyperspherical而非ultraspherical，但古典名称已沿用。
递推关系的数值稳定性陷阱
递推关系计算贝塞尔函数时，方向不同稳定性完全不同：正向递推对Y_n稳定但对J_n不稳定，反向则相反。原因是J_n随n增大趋于零（极小解），Y_n趋于负无穷；正向计算J_n时舍入误差会放大 Growing 的Y_n分量，导致结果崩溃。 Miller算法可稳定计算极小解。