How did humanity coax mathematics from the aether? We explore the Platonic
view that mathematics can be discovered from its axioms - a game of conjecture
and proof. We describe Minimo (Mathematics from Intrinsic Motivation): an agent
that jointly learns to pose challenging problems for itself (conjecturing) and
solve them (theorem proving). Given a mathematical domain axiomatized in
dependent type theory, we first combine methods for constrained decoding and
type-directed synthesis to sample valid conjectures from a language model. Our
method guarantees well-formed conjectures by construction, even as we start
with a randomly initialized model. We use the same model to represent a policy
and value function for guiding proof search. Our agent targets generating hard
but provable conjectures - a moving target, since its own theorem proving
ability also improves as it trains. We propose novel methods for hindsight
relabeling on proof search trees to significantly improve the agent's sample
efficiency in both tasks. Experiments on 3 axiomatic domains (propositional
logic, arithmetic and group theory) demonstrate that our agent can bootstrap
from only the axioms, self-improving in generating true and challenging
conjectures and in finding proofs.

通过构造一个 agent，它能够自我产生推测和证明，我们探索了从自有公理中探索数学的方法。使用约束解码和类型导向综合的方法，我们在依赖类型理论中对数学领域进行公理化，从中采样有效的推测，同时使用相同的模型生成策略和价值函数来引导证明搜索，从而生成难以证明但可证明的猜测，agent 能够从公理开始自我提高，并通过在证明搜索树上应用回顾重新标记等创新方法显著提高其样本效率，实验证明我们的 agent 能够从只有公理开始，自我提高产生真实且具有挑战性的猜测和找到证明。

从内在动机学习形式数学

Learning Formal Mathematics From Intrinsic Motivation

In 2021, Adam Zsolt Wagner proposed an approach to disprove conjectures in
graph theory using Reinforcement Learning (RL). Wagner's idea can be framed as
follows: consider a conjecture, such as a certain quantity f(G) < 0 for every
graph G; one can then play a single-player graph-building game, where at each
turn the player decides whether to add an edge or not. The game ends when all
edges have been considered, resulting in a certain graph G_T, and f(G_T) is the
final score of the game; RL is then used to maximize this score. This brilliant
idea is as simple as innovative, and it lends itself to systematic
generalization. Several different single-player graph-building games can be
employed, along with various RL algorithms. Moreover, RL maximizes the
cumulative reward, allowing for step-by-step rewards instead of a single final
score, provided the final cumulative reward represents the quantity of interest
f(G_T). In this paper, we discuss these and various other choices that can be
significant in Wagner's framework. As a contribution to this systematization,
we present four distinct single-player graph-building games. Each game employs
both a step-by-step reward system and a single final score. We also propose a
principled approach to select the most suitable neural network architecture for
any given conjecture, and introduce a new dataset of graphs labeled with their
Laplacian spectra. Furthermore, we provide a counterexample for a conjecture
regarding the sum of the matching number and the spectral radius, which is
simpler than the example provided in Wagner's original paper.
The games have been implemented as environments in the Gymnasium framework,
and along with the dataset, are available as open-source supplementary
materials.

提出了一种使用强化学习来反驳图论猜想的方法，通过单人图构建游戏来最大化游戏得分，并通过选择适当的神经网络结构和引入新的带有拉普拉斯光谱标签的图数据集，系统化地探讨了这种方法并提出了四种不同的单人图构建游戏。

瓦格纳框架的系统化：图论猜想与强化学习

A Systematization of the Wagner Framework: Graph Theory Conjectures and  Reinforcement Learning

In this paper we report on new results relating to a conjecture regarding
properties of $n\times n$, $n\leq 6$, positive definite matrices. The
conjecture has been proven for $n\leq 4$ using computer-assisted sum of squares
(SoS) methods for proving polynomial nonnegativity. Based on these proven
cases, we report on the recent identification of a new family of matrices with
the property that their diagonals majorize their spectrum. We then present new
results showing that this family can extended via Kronecker composition to
$n>6$ while retaining the special majorization property. We conclude with
general considerations on the future of computer-assisted and AI-based proofs.

通过计算机辅助的平方和方法证明，我们报道了关于 $n	imes n$ 阳性定义矩阵性质的猜想的新结果。基于已经证明的情况，我们发现了一类新的矩阵家族，其对角线主导其谱。我们还展示了这一家族可以通过 Kronecker 组合扩展到 $n>6$ 并保留特殊的主导性质。最后，我们对计算机辅助和基于人工智能的证明的未来进行了一般性的考虑。

关于频谱主导性质的部分猜想证明

Partial Proof of a Conjecture with Implications for Spectral  Majorization

Let $i_t(G)$ be the number of independent sets of size $t$ in a graph $G$.
Engbers and Galvin asked how large $i_t(G)$ could be in graphs with minimum
degree at least $\delta$. They further conjectured that when $n\geq 2\delta$
and $t\geq 3$, $i_t(G)$ is maximized by the complete bipartite graph
$K_{\delta, n-\delta}$. This conjecture has drawn the attention of many
researchers recently. In this short note, we prove this conjecture.

研究独立集的数量及其最大化问题，通过证明假设得出其在最小度至少为 δ 的完全二分图中实现最大化。