論文の概要: Compression is all you need: Modeling Mathematics

• arxiv url: http://arxiv.org/abs/2603.20396v1
• Date: Fri, 20 Mar 2026 18:16:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-24 19:11:38.886452
• Title: Compression is all you need: Modeling Mathematics
• Title（参考訳）: 圧縮は必要なもの - 数学のモデリング
• Authors: Vitaly Aksenov, Eve Bodnia, Michael H. Freedman, Michael Mulligan,
• Abstract要約: 人間の数学(HM)は階層的にネストされた定義、補題、定理を通じて圧縮性によって区別される。 私たちはこれらのモデルを、HMのプロキシとして捉えた大規模なLean4ライブラリであるMathLibに対してテストします。 包み長は, 深さと包み長の両方で指数関数的に増加し, 包み長は全深さにわたってほぼ一定である。
• 参考スコア（独自算出の注目度）: 0.4433169165028139
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Human mathematics (HM), the mathematics humans discover and value, is a vanishingly small subset of formal mathematics (FM), the totality of all valid deductions. We argue that HM is distinguished by its compressibility through hierarchically nested definitions, lemmas, and theorems. We model this with monoids. A mathematical deduction is a string of primitive symbols; a definition or theorem is a named substring or macro whose use compresses the string. In the free abelian monoid $A_n$, a logarithmically sparse macro set achieves exponential expansion of expressivity. In the free non-abelian monoid $F_n$, even a polynomially-dense macro set only yields linear expansion; superlinear expansion requires near-maximal density. We test these models against MathLib, a large Lean~4 library of mathematics that we take as a proxy for HM. Each element has a depth (layers of definitional nesting), a wrapped length (tokens in its definition), and an unwrapped length (primitive symbols after fully expanding all references). We find unwrapped length grows exponentially with both depth and wrapped length; wrapped length is approximately constant across all depths. These results are consistent with $A_n$ and inconsistent with $F_n$, supporting the thesis that HM occupies a polynomially-growing subset of the exponentially growing space FM. We discuss how compression, measured on the MathLib dependency graph, and a PageRank-style analysis of that graph can quantify mathematical interest and help direct automated reasoning toward the compressible regions where human mathematics lives.
• Abstract（参考訳）: 人間数学(Human mathematics, HM)は、人間が発見し、価値を与える数学であり、すべての有効な導出の総数である形式数学(FM)の極めて小さな部分集合である。 我々は、HMは階層的にネストされた定義、補題、定理を通じて圧縮性によって区別されると主張する。 私たちはこれをモノイドでモデル化します。 数学的推論は原始記号の文字列であり、定義や定理は文字列を圧縮する名前付きサブストリングまたはマクロである。 自由アーベルモノイド $A_n$ において、対数的にスパースなマクロ集合は表現性の指数展開を達成する。 自由非アーベルモノイド $F_n$ では、多項式密度のマクロ集合でさえ線型展開しか得られず、超線型展開は近似最大密度を必要とする。 私たちはこれらのモデルを、HMのプロキシとして捉えた大規模なLean~4の数学ライブラリであるMathLibに対してテストします。 各要素は深さ(定義ネストの層)、包まれた長さ(定義のトークン)、未開長(すべての参照を完全に拡張した後の原始記号)を持つ。 包み長は, 深さと包み長の両方で指数関数的に増加し, 包み長は全深さにわたってほぼ一定である。 これらの結果は$A_n$と一致し、F_n$と矛盾せず、指数的に増大する空間FMの多項式的に成長する部分集合をHMが占めるという理論を支持する。 そこで我々は,MathLib依存グラフで測定された圧縮と,そのグラフのPageRank型解析が数学的関心を定量化し,人間の生活する圧縮可能な領域への直接的自動推論を支援する方法について論じる。

関連論文リスト

• Expressive Power of Deep Networks on Manifolds: Simultaneous Approximation [2.815765641180636]
  境界重みを持つ定数深度$mathrmReLUk-1$ネットワークは、ソボレフ空間内の任意の関数を近似することができることを示す。 また、必要なパラメータ数が対数係数に一致することを示すことで、我々の構成がほぼ最適であることを示す。
  論文  参考訳（メタデータ） (2025-09-11T11:28:20Z)
• From Euler to AI: Unifying Formulas for Mathematical Constants [0.0]
  数式を体系的に統一する。 我々は、$pi$に対して407の異なる式を検証し、$pi$無限和の間の証明を行う。 我々の方法は$zeta(3)$を含む他の定数に一般化し、ドメイン間の知識を統一する。
  論文  参考訳（メタデータ） (2025-02-24T14:42:48Z)
• Llemma: An Open Language Model For Mathematics [46.557804525919785]
  数学のための大きな言語モデルであるLlemmaを紹介します。 MATHベンチマークでは、Llemmaはすべての既知のオープンベースモデルより優れている。 レムマは道具の使用と公式な定理を証明することができるが、それ以上の微調整は行わない。
  論文  参考訳（メタデータ） (2023-10-16T17:54:07Z)
• An Approximation Theory for Metric Space-Valued Functions With A View Towards Deep Learning [25.25903127886586]
  任意のポーランド計量空間 $mathcalX$ と $mathcalY$ の間の連続写像の普遍函数近似器を構築する。 特に、必要なディラック測度数は $mathcalX$ と $mathcalY$ の構造によって決定されることを示す。
  論文  参考訳（メタデータ） (2023-04-24T16:18:22Z)
• Low-degree learning and the metric entropy of polynomials [44.99833362998488]
  少なくとも$Omega(sqrtvarepsilon)2dlog n leq log mathsfM(mathscrF_n,d,|cdot|_L,varepsilon)は2辺の推定値$c(1-varepsilon)2dlogを満たす。
  論文  参考訳（メタデータ） (2022-03-17T23:52:08Z)
• Hardness of Learning Halfspaces with Massart Noise [56.98280399449707]
  我々は、マッサート(有界)ノイズの存在下でPAC学習のハーフスペースの複雑さを研究します。 情報理論上最適なエラーとSQアルゴリズムで達成できる最高のエラーとの間に指数関数的なギャップがあることを示した。
  論文  参考訳（メタデータ） (2020-12-17T16:43:11Z)
• Small Covers for Near-Zero Sets of Polynomials and Learning Latent Variable Models [56.98280399449707]
  我々は、s$ of cardinality $m = (k/epsilon)o_d(k1/d)$ に対して $epsilon$-cover が存在することを示す。 構造的結果に基づいて,いくつかの基本的高次元確率モデル隠れ変数の学習アルゴリズムを改良した。
  論文  参考訳（メタデータ） (2020-12-14T18:14:08Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。