OmegaInstituteOffical

Rebuilding math & physics from one act of distinction.
BEDC · Lean 4 · 0 axioms.

[OmegaInstituteOffical @OmegaDesci]

Thue–Morse 词是词组合里被研究得最多的对象之一,因为它的自相似总会变成一些很干净的规律。这是最近的一个。

这里研究的 Campbell–Currie–Rampersad 猜想与 Thue–Morse 词的 reduced abelian complexity R(n) 有关。对它的每个长度 n 因子,先做 run-compress,把每一段连续相同的字母压成一个;接着记录 Parikh 向量,也就是压缩后 0 和 1 各有多少。R(n) 统计这些向量共有多少种。这个量把局部的连续段结构与 Thue–Morse 著名的自相似性连在一起,因此一个干净的递推式会很有分量。

Thue–Morse 词内部藏着按比例缩小的自身结构。这种自相似在计数中留下了一个精确的“回声”:奇数长度 2n+1 处的复杂度,恰好等于长度 n+1 处的复杂度,像是把计数问题对折一半,答案仍然原样保留。我们证明了这个“对折”。

对所有 n,我们证明 R(2n+1) = R(n+1)。由此立刻得到,对每个 k ≥ 0,都有 R(2^k+1) = 3。这项定理给出奇数长度的递推;偶数长度的情形以及 non-automaticity 问题仍在此次结果范围之外。

结果已由 Lean 在 kernel 层核验,不含 sorry,并证明了 Lean 陈述忠实对应原命题。结果页:https://t.co/Pb5JWF1wSX

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

我们把一路积累下来的形式化工作汇总到了一座可交互的数学 Atlas 里。Lean 是贯穿上下游工程的唯一真源，站点则把这份经过核验的内容铺开，让人可以浏览，也可以顺着结构一路追下去。我们一直想从形式化结果里看见概念之间更深的连接，看看逻辑簇是怎样长出来的、概念会在哪里相遇。沿着这些连接继续走，也许还能看出哪些作用边牵动着更大的范围。

现在打开 Atlas，可以从几种不同的视角进入同一套内容。按类别铺开的 DAG 里，每个概念都可以点击；沿着上下游走，就能找到对应的概念 wiki，也能看到它与其他概念的关联。Dependencies 视图关注那些在不同领域反复出现的常数和参数，我们想从中找到最稳定、最不容易移动的 anchor。这件事很有意思，也给了我们不少启发：无论是最小化还是元语言，追到深处都绕不开同一个问题，那个“核心中的核心”究竟在哪里，什么才是最基础、最不动的东西。Open Problems 视图把我们正在 tackle 的开放问题接回已经形式化的概念，让一项正在推进的研究依托哪些基础、又会向 Atlas 的哪里延伸，逐渐变得可见。

接下来，我们想试着像优化蛋白质结构或 energy landscape 那样优化这张 DAG，让数学逻辑里潜藏的结构在过程中自行展现，并一步步演化出来。每一次 release 都会成为这条演化路径上的一个节点。Evolution 页面会记录这条路径，也会呈现 AI 在探索中自己选择的演化方向。

Research 页面收录我们最近的新成果，它们来自一套由我们自己 curate 的 open-problem / conjecture 库。我们会继续把真实的开放问题接入这套库，沿着这些桥梁推进求解。我们也希望，这些工作能为未来 ai4math 的形式化发展打下更扎实的基础。很高兴告诉大家，我们已经解出了其中一些 conjecture；接下来的几条 posts，会展开讲讲这些结果。

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

The Thue–Morse word is one of the most-studied objects in combinatorics on words, because its self-similarity keeps turning into clean patterns. Here is a recent one.

The Campbell–Currie–Rampersad conjecture studied here concerns the reduced abelian complexity R(n) of the Thue–Morse word. For every factor of length n, first run-compress it, replacing each maximal run of equal letters by a single letter; then record its Parikh vector, the pair counting how many 0s and 1s remain. R(n) is the number of distinct such vectors. This statistic blends local run structure with the celebrated self-similarity of Thue–Morse, making a clean recurrence especially striking.

The Thue–Morse word contains scaled-down copies of its own structure. That self-similarity leaves a precise echo in this count: at odd length 2n+1, the complexity is exactly the value at length n+1. It is as if the counting problem folds in half while retaining the same answer. We proved this fold.

For every n, we prove R(2n+1) = R(n+1). As an immediate consequence, R(2^k+1) = 3 for every k ≥ 0. The theorem establishes the odd-length recurrence; even-length behavior and the non-automaticity question remain outside this result.

The result was verified by Lean at the kernel level, with no sorry, including a proof that the Lean statement faithfully corresponds to the original proposition. Result page: https://t.co/Pb5JWF1wSX

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

We have brought our formalization work to date into an interactive publishing site: a mathematical Atlas. Lean remains the single source of truth carried through our upstream and downstream engineering, while the site turns that verified body of work into something people can browse and trace. We want to see how clusters of logic take shape and where concepts meet inside formalized mathematics. We also want to understand which edges exert more influence than others.

The Atlas currently offers several ways into the same body of work. Its category-organized DAG lets you click into any concept and trace its upstream and downstream connections to the relevant concept wiki and visual map of related ideas. The Dependencies view looks across fields for constants and parameters that keep recurring, with the aim of finding the most stable, least shifting anchors. We find this especially interesting because minimization and metalanguage keep returning to a similar search: the core within the core, the most fundamental structures that move the least. The Open Problems view draws bridges between the questions we are tackling and the concepts that have already been formalized, making it possible to see where current work attaches to the Atlas and what foundations it draws on.

Looking ahead, we want to explore whether this DAG can be optimized in a way that resembles the optimization of protein structures or an energy landscape, so that the structure latent in mathematical logic can reveal itself and evolve through the process. Each release is one step in that evolution. The Evolution page will make the path visible, including the paths AI chooses as it explores how the Atlas might develop.

The Research page gathers our latest results, drawn from an open-problem and conjecture library that we curate ourselves. We will keep connecting open questions to this library and working through them. Over time, we hope this will lay stronger foundations for the next stage of formal AI for mathematics. We are also glad to share that we have already solved some of these conjectures. The next few posts will go deeper into what we found.

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

有些序列是靠一条规则一步步、一直生成下去定义的,人们真正想知道的是:这样无穷地做下去,最后有没有一个简单的描述。这就是一个「有」的例子。

Bosma et al. Conjecture 17 出自 JIS 28 (2025), 25.3.8,研究一族带双参数 (g,d) 的贪心 3-sumfree 序列。从 (g,d) 决定的种子出发,每一步都收进最小的合格整数:它不能写成此前已经收进序列的三个不同整数之和。这个无限过程每一步只做局部检查,猜想却预言最终所有成员服从一个全局的周期公式。若能证明二者一致,判断一个数是否在序列里就可以直接套用公式。

可以把它想成逐步拉一份带编号的名单。每次只加入编号最小的合格者,条件是它不能与名单里已有的三个不同编号凑出禁配关系,也就是那三个数之和恰好等于它。照定义看,名单每加一项都要继续检查;猜想说完整名单其实落在周期性窗口里,一条公式就能直接描述。我们证明了逐步执行的贪心规则与这条公式给出同一份名单。

在 2 ≤ d 且 d+1 ≤ g 时,我们证明了精确的成员判据:z 属于该序列 ⟺ z ∈ {1, g, 2g+d−1, 2g+d},或 z 落在猜想给出的模 5g+2d 周期窗口中;同时证明这个闭式在每一步都与字面的贪心规则一致。例如,(g,d) = (3,2) 时,序列开头是 1, 3, 5, 6, 7, 8, 22, 23, 24, 25, 41, 42, 43, 44, 60;(g,d) = (5,3) 时,开头是 1, 5, 8, 9, 10, 11, 12, 13, 37, …。定理覆盖 2 ≤ d、d+1 ≤ g 的参数范围;以 g+1 为种子的另一支序列不在此次结果中。

结果已由 Lean 在 kernel 层核验,不含 sorry,并证明了 Lean 陈述忠实对应原命题。结果页:https://t.co/CdZNC8HKqf

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

我们把一路积累下来的形式化工作汇总到了一座可交互的数学 Atlas 里。Lean 是贯穿上下游工程的唯一真源，站点则把这份经过核验的内容铺开，让人可以浏览，也可以顺着结构一路追下去。我们一直想从形式化结果里看见概念之间更深的连接，看看逻辑簇是怎样长出来的、概念会在哪里相遇。沿着这些连接继续走，也许还能看出哪些作用边牵动着更大的范围。

现在打开 Atlas，可以从几种不同的视角进入同一套内容。按类别铺开的 DAG 里，每个概念都可以点击；沿着上下游走，就能找到对应的概念 wiki，也能看到它与其他概念的关联。Dependencies 视图关注那些在不同领域反复出现的常数和参数，我们想从中找到最稳定、最不容易移动的 anchor。这件事很有意思，也给了我们不少启发：无论是最小化还是元语言，追到深处都绕不开同一个问题，那个“核心中的核心”究竟在哪里，什么才是最基础、最不动的东西。Open Problems 视图把我们正在 tackle 的开放问题接回已经形式化的概念，让一项正在推进的研究依托哪些基础、又会向 Atlas 的哪里延伸，逐渐变得可见。

接下来，我们想试着像优化蛋白质结构或 energy landscape 那样优化这张 DAG，让数学逻辑里潜藏的结构在过程中自行展现，并一步步演化出来。每一次 release 都会成为这条演化路径上的一个节点。Evolution 页面会记录这条路径，也会呈现 AI 在探索中自己选择的演化方向。

Research 页面收录我们最近的新成果，它们来自一套由我们自己 curate 的 open-problem / conjecture 库。我们会继续把真实的开放问题接入这套库，沿着这些桥梁推进求解。我们也希望，这些工作能为未来 ai4math 的形式化发展打下更扎实的基础。很高兴告诉大家，我们已经解出了其中一些 conjecture；接下来的几条 posts，会展开讲讲这些结果。

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

Some sequences are defined by a rule you keep applying forever, one step at a time, and the open question is whether all that stepwise work has a simple description. Here is a case where it does.

Bosma et al. Conjecture 17, from JIS 28 (2025), 25.3.8, concerns a two-parameter family of greedy 3-sumfree sequences. Starting from seeds determined by (g,d), the construction repeatedly admits the smallest integer that cannot be written as the sum of three distinct terms already admitted. This is an infinite process governed by a local test at every step, yet the conjecture predicts a global periodic description of all its members. Establishing that bridge makes membership decidable directly from a formula.

Think of building a numbered roster one entry at a time. At each step, you add the smallest available number that cannot join three distinct numbers already on the roster to make the forbidden equation “their sum equals this new number.” A direct construction seems to require checking the roster forever. The conjecture says the completed roster actually falls into periodic windows, so a single formula tells you who appears. We proved that the step-by-step rule and the formula produce exactly the same roster.

For 2 ≤ d and d+1 ≤ g, we prove the exact membership criterion: z is a term ⟺ z ∈ {1, g, 2g+d−1, 2g+d} or z lies in the conjecture's periodic window modulo 5g+2d. We also prove that this closed form agrees with the literal greedy rule at every step. For (g,d) = (3,2), the sequence begins 1, 3, 5, 6, 7, 8, 22, 23, 24, 25, 41, 42, 43, 44, 60; for (g,d) = (5,3), it begins 1, 5, 8, 9, 10, 11, 12, 13, 37, …. The theorem applies when 2 ≤ d and d+1 ≤ g; the separate seed family involving g+1 lies outside its scope.

The result was verified by Lean at the kernel level, with no sorry, including a proof that the Lean statement faithfully corresponds to the original proposition. Result page: https://t.co/CdZNC8HKqf

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

We have brought our formalization work to date into an interactive publishing site: a mathematical Atlas. Lean remains the single source of truth carried through our upstream and downstream engineering, while the site turns that verified body of work into something people can browse and trace. We want to see how clusters of logic take shape and where concepts meet inside formalized mathematics. We also want to understand which edges exert more influence than others.

The Atlas currently offers several ways into the same body of work. Its category-organized DAG lets you click into any concept and trace its upstream and downstream connections to the relevant concept wiki and visual map of related ideas. The Dependencies view looks across fields for constants and parameters that keep recurring, with the aim of finding the most stable, least shifting anchors. We find this especially interesting because minimization and metalanguage keep returning to a similar search: the core within the core, the most fundamental structures that move the least. The Open Problems view draws bridges between the questions we are tackling and the concepts that have already been formalized, making it possible to see where current work attaches to the Atlas and what foundations it draws on.

Looking ahead, we want to explore whether this DAG can be optimized in a way that resembles the optimization of protein structures or an energy landscape, so that the structure latent in mathematical logic can reveal itself and evolve through the process. Each release is one step in that evolution. The Evolution page will make the path visible, including the paths AI chooses as it explores how the Atlas might develop.

The Research page gathers our latest results, drawn from an open-problem and conjecture library that we curate ourselves. We will keep connecting open questions to this library and working through them. Over time, we hope this will lay stronger foundations for the next stage of formal AI for mathematics. We are also glad to share that we have already solved some of these conjectures. The next few posts will go deeper into what we found.

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

组合里有不少开放问题,都是些看起来很朴素、底下却藏着结构的序列。这是我们最近解决的一个。

Chamberland–Dilcher Conjecture 2.1 研究序列 d(n,l) = ⌊√(2ln)⌋ − ⌊√((2l−1)n)⌋。这里的 floor 会抹去平方根的小数部分,所以每一项都在比较两条交错的“平方根台阶”。随着 l 变化,d(n,l) 有时会连续几项等于 0。这些零块记录了两条台阶恰好齐平的位置,而猜想预言,它们的出现与分隔有一套很整齐的规律。

可以想象自己沿一段台阶向上走,每一级的高度由一个 floor 平方根决定。多数时候高度继续上升,偶尔会卡住,形成一小段平的平台;序列里的连续 0 就是这些平台。猜想说,每个合格标签都对应一段平台,不同标签所指的平台彼此从不重叠。我们对奇数 n 证明了这个图景。

精确地说,对每个奇数 n,猜想中的每个合格标签 λ 都在 d 序列中对应一段连续的 0,而不同标签对应的零块两两不相交。例如,n = 21 时,相关序列为 [2, 2, 1, 0, 1, 0, 1, 1, 1, 1];n = 33 时,相关序列为 [3, 2, 2, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1, 1, 1]。这一定理的范围是奇数 n。

结果已由 Lean 在 kernel 层核验,不含 sorry,并证明了 Lean 陈述忠实对应原命题。结果页:https://t.co/RI47CKDXxf

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

我们把一路积累下来的形式化工作汇总到了一座可交互的数学 Atlas 里。Lean 是贯穿上下游工程的唯一真源，站点则把这份经过核验的内容铺开，让人可以浏览，也可以顺着结构一路追下去。我们一直想从形式化结果里看见概念之间更深的连接，看看逻辑簇是怎样长出来的、概念会在哪里相遇。沿着这些连接继续走，也许还能看出哪些作用边牵动着更大的范围。

现在打开 Atlas，可以从几种不同的视角进入同一套内容。按类别铺开的 DAG 里，每个概念都可以点击；沿着上下游走，就能找到对应的概念 wiki，也能看到它与其他概念的关联。Dependencies 视图关注那些在不同领域反复出现的常数和参数，我们想从中找到最稳定、最不容易移动的 anchor。这件事很有意思，也给了我们不少启发：无论是最小化还是元语言，追到深处都绕不开同一个问题，那个“核心中的核心”究竟在哪里，什么才是最基础、最不动的东西。Open Problems 视图把我们正在 tackle 的开放问题接回已经形式化的概念，让一项正在推进的研究依托哪些基础、又会向 Atlas 的哪里延伸，逐渐变得可见。

接下来，我们想试着像优化蛋白质结构或 energy landscape 那样优化这张 DAG，让数学逻辑里潜藏的结构在过程中自行展现，并一步步演化出来。每一次 release 都会成为这条演化路径上的一个节点。Evolution 页面会记录这条路径，也会呈现 AI 在探索中自己选择的演化方向。

Research 页面收录我们最近的新成果，它们来自一套由我们自己 curate 的 open-problem / conjecture 库。我们会继续把真实的开放问题接入这套库，沿着这些桥梁推进求解。我们也希望，这些工作能为未来 ai4math 的形式化发展打下更扎实的基础。很高兴告诉大家，我们已经解出了其中一些 conjecture；接下来的几条 posts，会展开讲讲这些结果。

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

A lot of open problems in combinatorics are about simple-looking sequences that quietly hide real structure. Here is one we recently settled.

Chamberland–Dilcher Conjecture 2.1 concerns the sequence d(n,l) = ⌊√(2ln)⌋ − ⌊√((2l−1)n)⌋. Each term compares two interlaced square-root staircases after their fractional parts have been discarded. As l varies, d(n,l) sometimes becomes 0 for several consecutive positions. Those zero blocks encode exact coincidences between the staircases, and the conjecture predicts a surprisingly orderly way to locate and separate them.

Imagine climbing a staircase whose level at each point is set by a floored square root. The level usually rises as you move, then occasionally sticks and creates a short flat stretch; those flat stretches are the consecutive zeros. The conjecture says every eligible label points to one such platform, and platforms carrying different labels never overlap. We proved that picture for odd n.

Precisely, for every odd n and every eligible label λ in the conjecture, the corresponding positions form a consecutive block of zeros in the d sequence, and the zero blocks attached to distinct labels are pairwise disjoint. For n = 21, the relevant values are [2, 2, 1, 0, 1, 0, 1, 1, 1, 1]. For n = 33, they are [3, 2, 2, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1, 1, 1]. The theorem covers odd n.

The result was verified by Lean at the kernel level, with no sorry, including a proof that the Lean statement faithfully corresponds to the original proposition. Result page: https://t.co/RI47CKDXxf

#Lean4 #AI4Math #FormalMath #Combinatorics #OEIS

[OmegaInstituteOffical @OmegaDesci]

We have brought our formalization work to date into an interactive publishing site: a mathematical Atlas. Lean remains the single source of truth carried through our upstream and downstream engineering, while the site turns that verified body of work into something people can browse and trace. We want to see how clusters of logic take shape and where concepts meet inside formalized mathematics. We also want to understand which edges exert more influence than others.

The Atlas currently offers several ways into the same body of work. Its category-organized DAG lets you click into any concept and trace its upstream and downstream connections to the relevant concept wiki and visual map of related ideas. The Dependencies view looks across fields for constants and parameters that keep recurring, with the aim of finding the most stable, least shifting anchors. We find this especially interesting because minimization and metalanguage keep returning to a similar search: the core within the core, the most fundamental structures that move the least. The Open Problems view draws bridges between the questions we are tackling and the concepts that have already been formalized, making it possible to see where current work attaches to the Atlas and what foundations it draws on.

Looking ahead, we want to explore whether this DAG can be optimized in a way that resembles the optimization of protein structures or an energy landscape, so that the structure latent in mathematical logic can reveal itself and evolve through the process. Each release is one step in that evolution. The Evolution page will make the path visible, including the paths AI chooses as it explores how the Atlas might develop.

The Research page gathers our latest results, drawn from an open-problem and conjecture library that we curate ourselves. We will keep connecting open questions to this library and working through them. Over time, we hope this will lay stronger foundations for the next stage of formal AI for mathematics. We are also glad to share that we have already solved some of these conjectures. The next few posts will go deeper into what we found.

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

最近 AI4Math 成果非常多,很激动看到越来越多人做出令人兴奋的贡献,这里也 share 几条我们最近的工作。第一条关于 Pochhammer Conjecture 6.5。算子 Lₐ 建立在下降阶乘,也就是 Pochhammer 基上;它可以看作普通单项式基在离散问题里的对应物。参数 c₂(a) 是一段参数范围的左端点:在这段范围内,多项式的复根全都落到实轴上,实部留在 [−1,0]。原猜想给出严格上界 c₂(a) < 2a,想要控制这些根能够移动到哪里。

可以把 a 想成一个可调旋钮,把 2a 想成 c₂(a) 理应始终严格压在下面的一条线。我们找到了精确的转换点:旋钮拨过 1/24 后,这项保证成立;拨到 1/24 时,c₂(a) 恰好触线;继续往下拨到 a ≤ 1/24,它就达到或越过原先声称的界。

在二次情形中,闭式分析给出精确等价关系 c₂(a) < 2a ⟺ a > 1/24。当 a = 1/24 时,c₂(a) = 1/12 = 2·(1/24);当 a ≤ 1/24 时,c₂(a) ≥ 2a。因此,原猜想的严格上界在小 a 区间失效,而 1/24 正是 sharp threshold。这项结果处理的是二次情形,高阶问题仍然开放。

结果已由 Lean 在 kernel 层核验,不含 sorry,并证明了 Lean 陈述忠实对应原命题。结果页:https://t.co/dRvdoGC4WY

[OmegaInstituteOffical @OmegaDesci]

我们把一路积累下来的形式化工作汇总到了一座可交互的数学 Atlas 里。Lean 是贯穿上下游工程的唯一真源，站点则把这份经过核验的内容铺开，让人可以浏览，也可以顺着结构一路追下去。我们一直想从形式化结果里看见概念之间更深的连接，看看逻辑簇是怎样长出来的、概念会在哪里相遇。沿着这些连接继续走，也许还能看出哪些作用边牵动着更大的范围。

现在打开 Atlas，可以从几种不同的视角进入同一套内容。按类别铺开的 DAG 里，每个概念都可以点击；沿着上下游走，就能找到对应的概念 wiki，也能看到它与其他概念的关联。Dependencies 视图关注那些在不同领域反复出现的常数和参数，我们想从中找到最稳定、最不容易移动的 anchor。这件事很有意思，也给了我们不少启发：无论是最小化还是元语言，追到深处都绕不开同一个问题，那个“核心中的核心”究竟在哪里，什么才是最基础、最不动的东西。Open Problems 视图把我们正在 tackle 的开放问题接回已经形式化的概念，让一项正在推进的研究依托哪些基础、又会向 Atlas 的哪里延伸，逐渐变得可见。

接下来，我们想试着像优化蛋白质结构或 energy landscape 那样优化这张 DAG，让数学逻辑里潜藏的结构在过程中自行展现，并一步步演化出来。每一次 release 都会成为这条演化路径上的一个节点。Evolution 页面会记录这条路径，也会呈现 AI 在探索中自己选择的演化方向。

Research 页面收录我们最近的新成果，它们来自一套由我们自己 curate 的 open-problem / conjecture 库。我们会继续把真实的开放问题接入这套库，沿着这些桥梁推进求解。我们也希望，这些工作能为未来 ai4math 的形式化发展打下更扎实的基础。很高兴告诉大家，我们已经解出了其中一些 conjecture；接下来的几条 posts，会展开讲讲这些结果。

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

There's a lot happening in AI for math right now, and it's genuinely exciting to see more people doing remarkable work in the field. We'd like to share a few of our own recent results. The first concerns Pochhammer Conjecture 6.5. Its operator Lₐ is built in the falling-factorial, or Pochhammer, basis, the discrete analogue of the usual monomial basis. The parameter c₂(a) is the left endpoint of the range in which the polynomial's complex zeros are forced onto the real axis while their real parts stay in [−1,0]. The conjecture proposed the strict bound c₂(a) < 2a, so it was asking for a uniform geometric constraint on where those zeros can go.

Think of a as an adjustable dial and 2a as a line that c₂(a) was expected to stay strictly below at every setting. We located the exact transition: the guarantee holds only after the dial passes 1/24. At 1/24 the quantity touches the line exactly, and at every setting a ≤ 1/24 it reaches or crosses the claimed bound.

For quadratic polynomials, the closed-form analysis gives the sharp equivalence c₂(a) < 2a ⟺ a > 1/24. At a = 1/24, c₂(a) = 1/12 = 2·(1/24); for a ≤ 1/24, c₂(a) ≥ 2a. Thus the proposed strict upper bound fails for small a, with 1/24 as the exact threshold. This result settles the quadratic case and leaves higher degrees open.

The result was verified by Lean at the kernel level, with no sorry, including a proof that the Lean statement faithfully corresponds to the original proposition. Result page: https://t.co/dRvdoGC4WY

[OmegaInstituteOffical @OmegaDesci]

We have brought our formalization work to date into an interactive publishing site: a mathematical Atlas. Lean remains the single source of truth carried through our upstream and downstream engineering, while the site turns that verified body of work into something people can browse and trace. We want to see how clusters of logic take shape and where concepts meet inside formalized mathematics. We also want to understand which edges exert more influence than others.

The Atlas currently offers several ways into the same body of work. Its category-organized DAG lets you click into any concept and trace its upstream and downstream connections to the relevant concept wiki and visual map of related ideas. The Dependencies view looks across fields for constants and parameters that keep recurring, with the aim of finding the most stable, least shifting anchors. We find this especially interesting because minimization and metalanguage keep returning to a similar search: the core within the core, the most fundamental structures that move the least. The Open Problems view draws bridges between the questions we are tackling and the concepts that have already been formalized, making it possible to see where current work attaches to the Atlas and what foundations it draws on.

Looking ahead, we want to explore whether this DAG can be optimized in a way that resembles the optimization of protein structures or an energy landscape, so that the structure latent in mathematical logic can reveal itself and evolve through the process. Each release is one step in that evolution. The Evolution page will make the path visible, including the paths AI chooses as it explores how the Atlas might develop.

The Research page gathers our latest results, drawn from an open-problem and conjecture library that we curate ourselves. We will keep connecting open questions to this library and working through them. Over time, we hope this will lay stronger foundations for the next stage of formal AI for mathematics. We are also glad to share that we have already solved some of these conjectures. The next few posts will go deeper into what we found.

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

我们把一路积累下来的形式化工作汇总到了一座可交互的数学 Atlas 里。Lean 是贯穿上下游工程的唯一真源，站点则把这份经过核验的内容铺开，让人可以浏览，也可以顺着结构一路追下去。我们一直想从形式化结果里看见概念之间更深的连接，看看逻辑簇是怎样长出来的、概念会在哪里相遇。沿着这些连接继续走，也许还能看出哪些作用边牵动着更大的范围。

现在打开 Atlas，可以从几种不同的视角进入同一套内容。按类别铺开的 DAG 里，每个概念都可以点击；沿着上下游走，就能找到对应的概念 wiki，也能看到它与其他概念的关联。Dependencies 视图关注那些在不同领域反复出现的常数和参数，我们想从中找到最稳定、最不容易移动的 anchor。这件事很有意思，也给了我们不少启发：无论是最小化还是元语言，追到深处都绕不开同一个问题，那个“核心中的核心”究竟在哪里，什么才是最基础、最不动的东西。Open Problems 视图把我们正在 tackle 的开放问题接回已经形式化的概念，让一项正在推进的研究依托哪些基础、又会向 Atlas 的哪里延伸，逐渐变得可见。

接下来，我们想试着像优化蛋白质结构或 energy landscape 那样优化这张 DAG，让数学逻辑里潜藏的结构在过程中自行展现，并一步步演化出来。每一次 release 都会成为这条演化路径上的一个节点。Evolution 页面会记录这条路径，也会呈现 AI 在探索中自己选择的演化方向。

Research 页面收录我们最近的新成果，它们来自一套由我们自己 curate 的 open-problem / conjecture 库。我们会继续把真实的开放问题接入这套库，沿着这些桥梁推进求解。我们也希望，这些工作能为未来 ai4math 的形式化发展打下更扎实的基础。很高兴告诉大家，我们已经解出了其中一些 conjecture；接下来的几条 posts，会展开讲讲这些结果。

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

We have brought our formalization work to date into an interactive publishing site: a mathematical Atlas. Lean remains the single source of truth carried through our upstream and downstream engineering, while the site turns that verified body of work into something people can browse and trace. We want to see how clusters of logic take shape and where concepts meet inside formalized mathematics. We also want to understand which edges exert more influence than others.

The Atlas currently offers several ways into the same body of work. Its category-organized DAG lets you click into any concept and trace its upstream and downstream connections to the relevant concept wiki and visual map of related ideas. The Dependencies view looks across fields for constants and parameters that keep recurring, with the aim of finding the most stable, least shifting anchors. We find this especially interesting because minimization and metalanguage keep returning to a similar search: the core within the core, the most fundamental structures that move the least. The Open Problems view draws bridges between the questions we are tackling and the concepts that have already been formalized, making it possible to see where current work attaches to the Atlas and what foundations it draws on.

Looking ahead, we want to explore whether this DAG can be optimized in a way that resembles the optimization of protein structures or an energy landscape, so that the structure latent in mathematical logic can reveal itself and evolve through the process. Each release is one step in that evolution. The Evolution page will make the path visible, including the paths AI chooses as it explores how the Atlas might develop.

The Research page gathers our latest results, drawn from an open-problem and conjecture library that we curate ourselves. We will keep connecting open questions to this library and working through them. Over time, we hope this will lay stronger foundations for the next stage of formal AI for mathematics. We are also glad to share that we have already solved some of these conjectures. The next few posts will go deeper into what we found.

Atlas: https://t.co/DedN5c7isU

[OmegaInstituteOffical @OmegaDesci]

我们看到,形式化已经成了 AI for math 里最重要、也不可或缺的一环。模型如今可以成批产出看起来相当合理的数学,真正让这些内容变得可信的,是把它们交给 kernel,一条条核验。我们相信,这一步已经从最后添上的一道保险,走到了整件事的核心。也正因为如此,我们在做 trureturing:一本 append-only 的真值账本。命题只有通过 kernel 核验才准入,要求 zero `sorry`、no `native_decide`,并且 axiom closure `⊆ {propext, Classical.choice, Quot.sound}`。模块一旦冻结,就永远不再改动;后续工作可以导入它,却不能回头重写它。目前已经冻结的内容包括 golden-integer tower,其中有 unit group `≃* ℤ × Multiplicative (ZMod 2)`、Fibonacci/Lucas bridges 和 prime splitting mod 5,也包括 zeta–Gibbs 与 entropy nodes。每个节点都经过 kernel 核验,并按内容寻址。

这条路也让我们在这周遇见了 TauCeti。按照他们公开的自述,TauCeti 是一个 downstream of Mathlib 的 AIs-welcome Lean library:AI 负责实现与评审,人类写 roadmap 和评审 rubric。我们开始做 trureturing 时并不知道 TauCeti,也没有和他们协作。后来发现另一个项目正从自己的方向走向同一个想法,这让我们觉得,让 AI 写形式化数学、再用核验机制把关,正在成为一种真实的工作方式。这周,我们在公开的 issue #5107 主动向他们打了招呼。

如果你也在做 AI 撰写的形式化数学,水温正好,欢迎下水。

Repo: https://t.co/B9eEqXB8C5
我们向 TauCeti 问好: https://t.co/I6zItbfhuo

[OmegaInstituteOffical @OmegaDesci]

We have watched formalization become one of the most important and indispensable parts of AI for math. Models can now produce vast amounts of mathematics that look remarkably plausible; what ultimately makes any of it trustworthy is handing it to a kernel for verification. We believe that step has moved from a useful finishing touch to the center of the whole endeavor. That belief is why we are building trureturing: an append-only ledger of mathematical truth in which a proposition is admitted only after kernel verification, with zero `sorry`, no `native_decide`, and axiom closure contained in `{propext, Classical.choice, Quot.sound}`. Once a module is frozen, it stays frozen. Later work may import it, but cannot rewrite it. The frozen ledger already includes the golden-integer tower, with the unit group `≃* ℤ × Multiplicative (ZMod 2)`, Fibonacci/Lucas bridges, and prime splitting mod 5, alongside zeta–Gibbs and entropy nodes. Every node is kernel-checked and content-addressed.

This week, that path led us to TauCeti. By its own public description, TauCeti is an AIs-welcome Lean library downstream of Mathlib: AI handles implementation and review, while humans write the roadmap and review rubric. When we started building trureturing, we did not know about TauCeti and had not collaborated with the project. Discovering another project working from the same underlying idea, in its own way, felt like a good sign that AI-written, kernel-verified mathematics is becoming a real way to work. We introduced ourselves this week in their public issue #5107.

If you are also working on AI-written formal mathematics, the water's fine. Come on in.

Repo: https://t.co/B9eEqXB8C5
Our hello to TauCeti: https://t.co/I6zItbfhuo

[OmegaInstituteOffical @OmegaDesci]

在 trureturing 里,我们一边推导,一边把其中一些结果整理成能在 mathlib 上形式化的数学。有些结果通用性够强,不只对我们自己有用,够格进 mathlib 本身——每到这种时候我们都挺开心。

最近的一个例子:两条引理合入了 Mathlib/NumberTheory/Wilson.lean。对素数 p 且 p % 4 ≠ 3,((p−1)/2)! 是 −1 模 p 的一个显式平方根——mathlib 本来有存在性定理和反方向判据,现在也有了具体的那个见证。底下的恒等式对任意奇数 p 都成立,不限于素数:

(p−1)! = (−1)^((p−1)/2) · (((p−1)/2)!)² 在 ZMod p 中,

这正是 Wilson 定理里的配对步骤。

我们真正在意的,是更广的社区参与,和一份能留下来的学术贡献——别人能在上面接着做、也能自己核验的数学。也希望更多人看到我们在 trureturing 里正在做的事,一起参与进来。

https://t.co/B9eEqXB8C5

[OmegaInstituteOffical @OmegaDesci]

In trureturing, as we work through our derivations, we keep turning parts of them into mathematics that can be formalized on top of mathlib. Some of that turns out general enough to flow back into mathlib itself, and it makes us happy when it does.

A recent example: two of our lemmas were merged into Mathlib/NumberTheory/Wilson.lean. For a prime p with p % 4 ≠ 3, ((p−1)/2)! is an explicit square root of −1 modulo p — mathlib had the existence theorem and the converse, and now it also carries the concrete witness. The identity underneath holds for every odd p, not only primes:

(p−1)! = (−1)^((p−1)/2) · (((p−1)/2)!)² in ZMod p

which is the usual pairing step in Wilson's theorem.

What we're really after is broader participation and a lasting academic contribution — mathematics that other people can build on and check for themselves. We'd love more people to see what we're doing in trureturing and take part.

https://t.co/B9eEqXB8C5

[OmegaInstituteOffical @OmegaDesci]

又一个阶段性工作见刊了。

我们送进同行评审的工作，也陆陆续续走到了最后几个环节。整个过程很有意思，也确实有点心酸。反复检查证明，等一轮新的意见，觉得已经收尾却又发现细小漏洞，再回到同一个论证上，有时候像是在一点点学会接受自己的不确定。能走到今天，靠的常常只是把问题一次次重新打开，再认真看一遍。

我们用 ChatGPT 已经一年多了。从零开始，慢慢摸到了一些可以站得住的结果。这篇论文是那段经历留下的一小块记录，也记录了我们怎样在自己的科研中使用 AI。它的范围很具体：一个标准化问题，以及几项我们反复核过的结论。对我们而言，它也记录了很长时间的尝试和细节核对，包括几次推倒重来之后，最后做成了什么。

我们觉得，科研也许会逐渐向没有走过常规路径的人打开。也许会有更多人真正获得做研究的机会，并在处理自己感兴趣的问题时学习。我们也在想，AI 工具是否可能降低一部分知识门槛，包括过去通常依赖大学训练的高等数学。未来，“专业人士”的边界也许会松动。现在也有不少人在讨论，基础模型是否可能在更多场景中替代专用模型。科研可能因此经历很大的变化；我们还不知道会走到哪里，但想继续观察，也继续做下去。

这篇新近见刊的论文题目是《Canonical Zeckendorf Normalization and Sharp Iteration Depth of the Berstel Adder》，发表于同行评审期刊 RAIRO – Theoretical Informatics and Applications，第 60 卷（2026）。

Zeckendorf 表示是一种用斐波那契数作位权的记数法。每个非负整数都有且只有一种写法，可以表示成若干个互不相邻的斐波那契数之和，因此表示它的 0/1 数位中不会出现相邻的两个 1。把两个这样的表示逐位相加后，中间结果可能出现 2，也可能出现相邻的 1，所以还要化回唯一的标准形。

论文通过经典的 Berstel 加法器研究这个标准化过程。对于两个合法 Zeckendorf 表示逐位相加得到的、长度为 n 的真实输入，从高位向低位读取并反复进行 Berstel 重新编码，达到贪心 Zeckendorf 标准形的最坏深度恰好是 ⌈n/2⌉。这个界是紧的，而且达到最大值时，n 就是输入的实际有效长度，不需要补前导零。

把方向倒过来，从低位向高位读取，情况就完全不同了。不存在一台按这个方向读取、顺序产生输出、末尾输出长度有界的确定性单遍有限状态转导器，能够对所有输入给出标准 Zeckendorf 形式。论文还给出了更强的定量结论：无论允许多少固定前瞻，某个给定的低位输出数位仍然可能无法确定。两个方向之间的这种不对称，是形式化证明完成之后，仍然让我们印象很深的部分。

对我们来说，这篇论文也保存着许多很普通的时刻。有些时候确实很开心，有些时候则会怀疑一个证明是否值得继续，或者它是不是经不起别人仔细看。见刊之后，那种不确定感还在。现在，别人可以仔细检查这项工作，再判断其中是否有值得继续做下去的东西。对目前这个阶段来说，这已经足够了。

我们也想找愿意一起探索数学推理、记数系统以及 AI for science 的朋友合作。手头还有一批论文准备投 arXiv。我们是新用户，目前需要 cs/math 分类的 endorsement。如果你愿意，欢迎先看看我们的 GitHub，再决定是否愿意为这些投稿背书。也欢迎任何觉得有合适切入点的人来联系，我们很愿意认真聊聊。

GitHub: https://t.co/Mt7OYdKK0I

DOI: https://t.co/T7RT1kE5Yo

[OmegaInstituteOffical @OmegaDesci]

Another stage of our work has now been published.

The work we have in peer review has been moving, one paper at a time, toward its final stages. The process has been genuinely interesting, and it has also been painful in ways that are hard to explain from the outside. There is a quiet kind of exhaustion in checking a proof again, waiting through another round of review, finding a gap after believing you were finished, and returning to the same argument with a little less certainty and a little more care.

We have been using ChatGPT for more than a year. We started close to zero and have slowly found a few results that we can stand behind. This paper is one small record of that journey and of how we have been using AI in our own scientific work. Its scope is narrow: one normalization problem, with claims we have checked carefully. For us, it also documents what became possible after spending a long time trying ideas and checking the details, including several restarts.

We think research may become more open to people who have not followed the usual route. Perhaps more people will get a real chance to learn by working on a question they care about. We wonder whether AI tools may lower some barriers to knowledge, including parts of advanced mathematics that have usually required university training. The boundary around the word “specialist” may loosen too. There is also an active discussion about whether foundation models may replace specialized models in more settings. Research may be approaching a major change; we do not yet know how far it will go, but we want to keep watching and working through it.

Our newly published paper is titled “Canonical Zeckendorf Normalization and Sharp Iteration Depth of the Berstel Adder.” It appears in the peer-reviewed journal RAIRO – Theoretical Informatics and Applications, volume 60 (2026).

Zeckendorf representation is a numeral system whose place values are Fibonacci numbers. Every nonnegative integer has a unique representation as a sum of non-adjacent Fibonacci numbers, so its 0-1 digit string has no adjacent 1s. When two such representations are added digit by digit, the intermediate word can contain 2s and adjacent 1s. It then has to be returned to its unique canonical form.

The paper studies that normalization problem through the classical Berstel adder. For genuine digitwise sums of two admissible Zeckendorf inputs of length n, read from the high Fibonacci positions toward the low positions, repeated Berstel recoding reaches the greedy Zeckendorf form in a worst-case depth of exactly ⌈n/2⌉. This bound is sharp, and the maximum is attained using the input’s actual significant length, with no leading-zero padding.

Reading in the opposite direction, from low positions toward high positions, has a fundamentally different behavior. No deterministic one-pass finite-state transducer, reading in that order and producing output sequentially with bounded terminal output, can always return the canonical Zeckendorf form. The paper proves a stronger quantitative obstruction: for any fixed amount of lookahead, even a given low-order output digit can remain undecided. The asymmetry between the two directions is the part that stayed with us after the formal statements were complete.

For us, this paper carries the memory of many ordinary hours. Some were satisfying. Some were spent wondering whether a proof was worth pursuing, or whether an error would appear as soon as someone else looked closely. That uncertainty is still with us after publication. Other people can now examine the work closely and decide whether there is anything here to build on. That is enough for this stage.

We would like to collaborate with people interested in mathematical reasoning, numeration systems, and AI for science. We also have a batch of papers that we hope to submit to arXiv. We are new users and need endorsement for submissions in the cs and math categories. Please look through our GitHub first and decide for yourself whether the work is worth endorsing. We would also be glad to hear from anyone who sees a useful way to work together.

GitHub: https://t.co/Mt7OYdKK0I

DOI: https://t.co/T7RT1kE5Yo

[OmegaInstituteOffical @OmegaDesci]

AI 给答案很快。答案出来以后，麻烦才真正开始：怎么确认它没错？即便没错，又凭什么说它重要？我们做 Omega Institute，大量时间其实花在这两个问题上。机器不缺产出，难的是验证，更难的是判断什么值得留下。

先说工作是怎么组织的。fkst（https://t.co/3ZDv2rS7Ol）按事先写明的章程协调 AI 智能体；一项工作从哪里来，经过了什么步骤，最后落到哪里，都要能追到源头。到了数学这一边，检验很直接：机器认定自己发现了结果，就交给 Lean。

一路上的尝试、误判和返工，主要留在 automath、newmath 和 trureturing 这三个仓库里。

automath（71★，~9,200 次 commit）是一套可审计的理论编译器。起点有条硬约束：观察一个系统时，只能使用有限的二进制窗口。窗口往外扩，读数仍然稳定的部分才留下。最后指向 golden-mean shift，它的特征方程是 x²=x+1。我们仍在写相应的 Lean 4 证明和论文稿。

仓库目前有 23,304 条定理和引理声明，~302k 行代码。用户声明的 axiom/sorry/admit 为零，CI 持续审计这一点。论文稿中带标签的论断共有 12,989 条，其中 7,877 条匹配到了 Lean 声明，占 60.6%（7,877/12,989）。我们宁可原样报数，也不拿“已形式化”的徽章当交代。

十二篇论文稿都有投稿记录，其中包括 DCDS-A 和 Journal of Number Theory 发放的投稿系统编号。有一篇收到审稿意见，修改后再次提交。现状也写清楚：零录用，两次拒稿。十二篇都没有发到 arXiv，也都没有 DOI。仓库里留着两次拒稿的记录，还留着两个定理缺陷。文字审阅漏掉了它们，形式化把它们抓了出来。

newmath 问的是另一个问题：不用 mathlib，同一套引擎会怎么样？从等式到实数，需要的接口全部重新搭建，没有直接导入。这个仓库有 38,065 条定理声明，649k 行自行编写的 Lean。曾经有一轮检查，Lean 用 72 小时查了其中 1,837 条声明。

后来我们把这些体量拆开看，发现不少内容只是既有陈述的机械变体。有的是参数重复，有的是增加元数；有些定理形态甚至已经被穷举。整个仓库可以从头构建，axiom 检查也没有报错。不过，这些检查只能说明它按规则写成了，不能回答这批语料到底有没有用。做到 38,000 个定理时，我们才真正看清瓶颈在哪。产出从来不缺，难的是筛选。

我们因此改了工作流。trureturing 是一本定理冻结账本，只能追加，已有记录不能改，记录之间用哈希链串接。每次冻结都要绑定定理的 statement IDs、axiom 闭包、源码 blob、来源 commit 和工具链字节。合并前会跑 23 条 lint。它们会拦住三种情况：闭合的定理依赖了尚未证明的结果；冻结载荷无法逐字节精确匹配；文字镜像偏离形式化陈述。最初三周，仓库一共记录了 441 个 PR，其中 410 个已经合并；同一时期冻结了 90 个模块，合计 1,052 条声明。

下一步是把这些冻结记录排成一张 DAG。图里既要标明哪些内容经过了 Lean 检查，也要把概念之间的联系显出来。一个概念如果在图中反复出现，也许说明背后还有更一般的东西。我们会把这层意思记下，但会注明尚未证实。这是判断，不是定理。

生物学这边也刚刚起步。我们试着用同一套方法处理包括 DNA 序列在内的数据，看到了一些值得继续查的模式，但暂时只能说到这里。眼下的假设是：面对微观和宏观系统，或许都可以问同一个问题——某种模式以投影形式出现的频率有多高？我们相信这个假设，但它还不是结果。接下来仍按同样的标准检验。

这些仓库全部公开，就是为了让人挑错。请直接检查，也请告诉我们，这项工作究竟错在哪里。

https://t.co/qcQqDdVyXF

[OmegaInstituteOffical @OmegaDesci]

Toward AI for mathematics, and a little more.

As we worked more deeply with AI, one question kept returning: when a machine gives us a result, how do we know it is correct, and how should we judge its importance? Correctness and evaluation came before output.

We followed that question in two directions. One was orchestration: fkst (https://t.co/3ZDv2rS7Ol) coordinates AI agents under a fixed constitution and keeps their work traceable to its sources. The other was mathematics as a proving ground, where Lean lets us check what we think we have found.

The clearest record is in three repositories, including the mistakes and corrections.

automath (71★, ~9,200 commits) is an auditable theory compiler. It starts from one forced constraint: observe a system through a finite binary window and retain only the readouts that remain stable as the window widens. Those stable readouts lead to the golden-mean shift with characteristic equation x² = x + 1. The project develops the consequences in Lean 4 and in manuscripts.

The repository contains 23,304 theorem and lemma declarations and about 302,000 lines, with zero user-declared axiom, sorry, or admit; a CI audit checks that condition. Of 12,989 labeled manuscript claims, 7,877 (60.6%) are matched to a Lean declaration. I'd rather quote that number than a badge.

Across twelve manuscripts, we have submission records, including portal IDs issued by DCDS-A and the Journal of Number Theory. One revision was resubmitted after a referee report. So far, there have been zero acceptances and two recorded rejections, and none of the manuscripts has an arXiv posting or DOI. The repository includes records of both rejections and of two theorem defects that formalization caught after prose review missed them.

newmath tested the same engine without mathlib. It rebuilt the interfaces it used, from equality through the real numbers, instead of importing them. The repository contains 38,065 theorem declarations across 649,000 lines of our own Lean; 1,837 of those declarations were checked by Lean during one 72-hour stretch.

We then examined what that volume consisted of. Much of it came from mechanically generating variations of existing statements by echoing parameters or expanding arity. Some theorem shapes had already been exhausted. A clean build and a passing axiom check did not by themselves make the corpus useful. Producing 38,000 theorems is how we learned that the bottleneck was never production. It was selection.

That lesson changed the workflow. trureturing is an append-only, hash-chained ledger for theorem freezes. Each freeze binds the theorem's statement IDs, axiom closure, source blob, origin commit, and toolchain bytes. Its 23 lint rules block a merge if a closed theorem depends on an unproved result, a freeze payload fails an exact byte match, or the prose mirror has drifted from the formal statement. During its first three weeks, the repository recorded 441 PRs, of which 410 were merged, and 90 frozen modules containing 1,052 declarations.

The ledger is meant to support a dependency graph showing what Lean has checked and how the concepts connect. If a concept keeps recurring across the graph, we want a way to record our confidence that it points to something more general without presenting that confidence as a theorem.

We are also beginning to apply this approach to biology, including DNA sequence data, where we have seen patterns worth investigating. One hypothesis is that microscopic and macroscopic systems can be studied with the same question: how often does a pattern appear as a projection? That is a belief, not a result, and we will hold it to the same standard as the rest.

The repositories are public because we want people to inspect the work and point out where it fails. https://t.co/qcQqDdVyXF

[OmegaInstituteOffical @OmegaDesci]

Hi Dominik — I'm Wenlin, a PhD student working on AI at NUS. Your posts on getting the n=3 Kemeny hardness result with GPT and then formalizing it in Lean are the closest thing I've seen to how we actually work, so I wanted to reach out.

I run a project called Omega Institute with Haobo Ma, the CEO of ChronoAI — really just the two of us, betting early on AI-driven mathematics. In one line: we formalize math in Lean, lay the derivations out as a dependency graph, and mine that graph for relationships nobody had noticed. It runs as an automated pipeline that's now producing a stack of papers heading to journals and arXiv.

Looking at your GitHub — SocialChoiceLean, HardnessReductionsLean, KemenyHardnessLean — you're building exactly the kind of Lean corpus we've spent the last year building infrastructure around. You've written about how fragile it is to shepherd LLMs through these reductions and how hard they are to simplify. That's the specific problem we attack: an adversarial agent that tries to break each proof before it's accepted, plus an append-only "truth ledger" that only admits machine-checked results, so an LLM-generated corpus keeps growing without silently rotting.

So here's a concrete thing I'd love to try together: put your social-choice / hardness Lean corpus behind our verification-and-ledger pipeline, so your reductions become one growing, provenance-tracked, drift-proof library instead of separate repos — and then run our graph-miner over the voting axioms to see whether it surfaces any unnoticed relationships between the impossibility results. Your mathematics, our accumulation engine. I'd treat it as an experiment, not a promise.

And one practical ask: we have a pipeline of papers heading to arXiv and are brand new there, so we need an endorsement to submit under the cs categories — from your record you'd be eligible. I'd rather you look at our GitHub first (https://t.co/qcQqDdVyXF) and only endorse if it seems worth it.

Either way, thank you for working in the open. It's been genuinely useful to watch.

[OmegaInstituteOffical @OmegaDesci]

我们有一篇新论文被 RAIRO – Theoretical Informatics and Applications 接收了。这是一本做理论计算机的同行评审期刊，论文之后会正式刊出。

先说它在算什么。

Zeckendorf 表示可以粗略看成“斐波那契进制”：每个非负整数都能唯一地写成若干个不相邻斐波那契数的和。两个数逐位一加，中间结果往往不合规：有的位会变成 2，也可能冒出相邻的 11。所谓 normalization，就是把这些冲突一路清掉，回到唯一的标准写法。

论文里有个很短的例子。按 1、2、3、5、8 的顺序把低位放在左边，4 写成 (1, 0, 1, 0, 0)，6 写成 (1, 0, 0, 1, 0)。逐位相加是

(2, 0, 1, 1, 0)，

里面既有 2，也有相邻的 11。归一化之后变成

(0, 1, 0, 0, 1)。

前后的值都是 10。

真正值得捋一捋的，是清理过程中的信息传播。

从高位往低位读，经典的 Berstel 加法器给出了一条有限状态的路。这台机器跑一遍，会先得到一个等值的二进制斐波那契表示；输出里还可能留着相邻的 11，所以要继续跑，直到进入唯一的贪心标准形。

这篇论文证明，对长度为 n 的真实加法输入，最坏情况刚好需要 ⌈n/2⌉ 趟。论文给出了达到这个上界的显式输入，而且不靠前导零来凑长度。精确常数和极值输入都由此确定。

可要是从低位往高位读，事情就麻烦了。对任意一个固定的输出位，机器看得再远也不够：总能找到两个真实的加法输入，它们在已读到的整段前缀上完全一样，等更远处的数位出现后，那个输出位的最终结果却会不同。

所以在这个方向上，带有有界终止输出的确定性一遍有限状态机器无法完成标准化；换成术语说，有限状态的 subsequential transducer 做不到。论文还把这个障碍算得更细：有些输入前缀读完时，当下看到的规范化输出一位都不能提前确定。再往后接输入，长度为 n 的输出前缀在最坏情况下可以全部被推翻。

我们最在意的就是这个方向上的不对称。高位先读，有经典的有限状态方法，清理深度也能精确算出来。低位先读，哪怕只想定下一个标准输出位，也可能要等任意远处的输入。

文中还顺手理清了一个容易说混的状态数问题。经典 Berstel 表里的 10 个状态，作为 raw complete-output residuals 时两两不同。做完标准的输出延迟归一化后，同一个函数得到一个 6 状态商；在允许初始输出词的 subsequential 模型中，这个商已经最小。

顺带说说这篇论文和 Omega 的关系。

Omega Institute 做 AI for mathematics。我们现在同时维护好几个库，不急着把所有东西收成一条路线。每个库使用不同的方法，分别探索两个问题：机器到底该怎么做数学，我们又该怎样核验它的结果。范围从 kernel 级的形式化证明，一直到离散结构上的自动推理。中间试过不少办法，走不通的也有。我们还在决定继续哪些方向。

这篇论文来自其中一个研究方向。

我们的内部规矩是：机器核验不了，暂时就不算数。这篇论文也单独接受了期刊的同行评审。我们既重视机器核验，也重视同行评审。

尺度也得讲清楚。这篇文章只研究一个具体运算，不延伸到关于 AI 与数学的宏大判断。

老实说，我们不算传统学术团队。团队里受过正规数学训练的人很少，很多东西是靠 AI 一边学一边做，走弯路的时候也不少。我们自己还在学。

论文已经按正常流程进了期刊。可轮到我们自己往 arXiv 传预印本，反倒卡在一件很初级的事上：我们是新用户，想投 cs / math 分类，需要 endorsement。

如果你具备这些分类的 endorsement 资格，也愿意考虑帮忙，欢迎先去 GitHub 看一眼，知道我们到底想做什么，再判断是否愿意 endorse 我们这次投稿。看过以后不愿意 endorse，也完全合理。

论文：《Canonical Zeckendorf Normalization and Sharp Iteration Depth of the Berstel Adder》，即将刊于 RAIRO – Theoretical Informatics and Applications

GitHub: https://t.co/Hz42sgQDkQ