指#20 @geelaw

@geelaw

这个算是标答了。以及#19 提到了同样一篇文章

应该只是定义不同，无关对错，哪里来的 python 精神可敬。。以下是 Lean 中求余的表达，官方也解释早期用 truncation-rounding 定义，后来用的 euclidean 定义。表达数学能力有差别，所以才改。

这篇文章解释了几种定义下的除法和求余
https://dl.acm.org/doi/pdf/10.1145/128861.128862

```lean4
-- default (guess using emod as default)
#eval (-1: Int) % (3: Int) -- 2
#eval (1: Int) % (-3: Int) -- 1

-- using emod (euclidean division)
#eval (-1: Int).emod (3 : Int) -- 2
#eval (1: Int).emod (-3 : Int) -- 1

-- using tmod (truncating division)
#eval (-1 : Int).tmod (3 : Int) -- -1
#eval (-1 : Int).tmod (-3 : Int) -- -1
```

页面可以啊

4->7->12->15 （渠道商买的坏了 1 年换 15p ） 平均 4 年一换吧

2. 共有模块（中台，路由 and 文件系统）有可能公用，对接 API 就行
3. 前端只是给客户看的，团队也有权限编辑自己的产品文档。
4. 我也好奇计费

1. 你列出的每一个产品都不止一个单独团队

Catppuccin Latte （喜欢紫色💜可以看看

@edwardzcn98 排版好像乱掉了，对这个感兴趣的话可以看一下这篇中文 blog： https://huggingface.co/blog/zh/winning-aimo-progress-prize

无意义去讨论是否通过图灵测试或者有没有智能这些。

可以合理怀疑目前最好的数学模型也是靠人力堆起来的（让模型去学习严格的机器推理+证明），他们的训练集覆盖了你给出的第一题。

Something relevant information

```
Project Numina is hiring Lean 4 contributors to work on formalizing competitive math problems and proofs! If you're passionate about mathematics, formal methods, and contributing to groundbreaking AI research, this could be the perfect opportunity for you.
Project Numina is a non-profit dedicated to advancing human and AI capabilities in mathematics. They've already achieved remarkable milestones:
```

补充资料：
Hugging Face 上[Numina 项目获得了第一届 AIMO 进步奖]( https://projectnumina.ai/publications/)，也发布了相关数学解题模型。

公开的在近 AI 领域你可能看不到他们联合数学家所做的努力，但是你会发现 Advisory Committee 下有 Tao 和另外几名 Lean FRO （包括语言的发明者）。

这是教学向的帖子吗？我看思路就和 toy message queue 一样。

@cleverlong 没懂

@seanzxx 。。拿 MacBook 也没成功，怀疑有非同名文件才行，午饭后再试一下。

@seanzxx 刚刚拿 mac mini 试了下，按住左/右 option 拖动 B 里面的 A 到外层 A 还是只有 Replace 弹框。
是我的姿势错了吗（用的外置键盘）

https://i.imgur.com/Nk20f4w.png

你问的全量增量捕获稳定性是做变更数据捕获工具测试比较麻烦的事，开源方案 2l 提到了 Flink CDC ，如果觉得不够定制或者需要改可以直接用下面封装的 Debezium

https://www.tradingview.com/blog/en/category/charting-library/

可以去 trade view 上面看看👀？

我是单反换的微单 a7c 一代，因为出去旅游爬山拍风景扛着三脚架太累了。a7c2 性价比比 1 代好，不吃灰就不亏。