Доказательства

Что именно доказано в Lean4

В репозитории Balansis лежит формальный слой на Lean 4 с Mathlib. Ниже — не пересказ бейджа из README, а результат прогона: 73 теорем собраны компилятором, у каждой запрошено #print axioms, и ни одна не опирается ни на что, кроме трёх стандартных аксиом Mathlib.

сборка и аудит: 4 шага, все с кодом 0leanprover/lean4:v4.28.0Mathlib v4.28.0 · 8f9d9cff6bПроверено 2026-09-08

Статус проверки

73теорем в публичном фасаде ACT

73/73получили отчёт #print axioms от ядра Lean

0теорем вне стандартной аксиоматики Mathlib

Стандартная аксиоматика здесь — это ровно три аксиомы: Classical.choice, Quot.sound, propext. Их использует практически любая работа с Mathlib; ничего специфичного для Balansis в этот список не добавлено. Отдельная проверка исходников: в 16 файлах formal/ нет вхождений sorry, admit и объявлений axiom.

Команды прогона аудита и их коды возврата. Прогон выполнен 2026-09-08 на той же машине, что и бенчмарки. Выполнено 2026-09-08
Команда	Код возврата	Длительность
`lake build BalansisFormal`	0	4.6 с
`lake build ACT`	0	3.7 с
`lake env lean FormalAudit.lean`	0	39.2 с
`lake env lean <tmp>/SiteAxiomAudit.lean`	0	26.8 с

Что означают эти цифры и чего они не означают. Из 73 теорем содержательно самостоятельна группа ExtendedRatio: семантика вырожденных состояний в ℝ не существует, и доказывать её приходится с нуля (включая утверждение о том, что носитель ExtendedRatio полем не является). Группы алгебры и анализа — перенос структуры ℝ через toReal/fromReal: доказано, что перенос корректен. Счётчик «73» складывает и то и другое, поэтому читать его как «73 независимых результатов» не следует.

Граница честности — главное на этой странице. Lean доказывает алгебру идеализированной модели, изоморфной вещественным числам (величина из NNReal плюс направление). Он не доказывает, что Python-код Balansis устойчив в арифметике float64, и не проверяет саму реализацию. Python и Lean здесь — две независимые реализации одной математической теории; связь между ними поддерживается тестами на паритет семантики, а не выводом кода из доказательств. Формулировка «библиотека формально верифицирована» была бы преувеличением: формально верифицирована теория, на которой библиотека построена.

Что доказано, по группам

A1–A5 · AbsoluteValue — 6 теорем, formal/ACT/Absolute.lean

Существование и единственность представления вещественного числа, неотрицательность величины, компенсация, аддитивная единица и сохранение направления.

Теорема	Формулировка в исходнике	Аксиомы
`a1_exists_unique`	`a1_exists_unique (x : ℝ) : ∃! a : AbsoluteValue, AbsoluteValue.toReal a = x`	стандартные 3
`a2_nonneg`	`a2_nonneg (a : AbsoluteValue) : (0 : ℝ) ≤ (a.magnitude : ℝ)`	стандартные 3
`a3_compensation`	`a3_compensation (a b : AbsoluteValue)`	стандартные 3
`a4_additive_identity`	`a4_additive_identity (a : AbsoluteValue) : a + AbsoluteValue.absolute = a`	стандартные 3
`a4_additive_identity_left`	`a4_additive_identity_left (a : AbsoluteValue) : AbsoluteValue.absolute + a = a`	стандартные 3
`a5_direction_preservation`	`a5_direction_preservation (a : AbsoluteValue) (c : ℝ)`	стандартные 3

E1–E4 · EternalRatio — 5 теорем, formal/ACT/EternalRatio.lean

Корректность отношения как фактор-типа, устойчивость при масштабировании, мультипликативная единица и обратимость.

Теорема	Формулировка в исходнике	Аксиомы
`e1_well_defined`	`e1_well_defined (a b : AbsoluteValue) (hb : b ≠ 0) :`	стандартные 3
`e2_stability`	`e2_stability (r : EternalRatio) :`	стандартные 3
`e3_multiplicative_identity`	`e3_multiplicative_identity (r : EternalRatio) : r * unity = r`	стандартные 3
`e3_multiplicative_identity_left`	`e3_multiplicative_identity_left (r : EternalRatio) : unity * r = r`	стандартные 3
`e4_inverse`	`e4_inverse (r : EternalRatio) (hr : r ≠ zero) : r * r⁻¹ = unity`	стандартные 3

S1–S3 · алгебраические законы — 22 теорем, formal/ACT/Algebra.lean

Аддитивные и мультипликативные законы, дистрибутивность и полевые структуры: инстансы Field для AbsoluteValue и для EternalRatio. Структура здесь перенесена из ℝ через toReal/fromReal — проверяется точность переноса, а не новая алгебра.

Теорема	Формулировка в исходнике	Аксиомы
`s1_closure`	`s1_closure (a b : AbsoluteValue) : ∃ c : AbsoluteValue, c = a + b`	стандартные 3
`s1_associativity`	`s1_associativity (a b c : AbsoluteValue) : (a + b) + c = a + (b + c)`	стандартные 3
`s1_commutativity`	`s1_commutativity (a b : AbsoluteValue) : a + b = b + a`	стандартные 3
`s1_identity_right`	`s1_identity_right (a : AbsoluteValue) : a + 0 = a`	стандартные 3
`s1_identity_left`	`s1_identity_left (a : AbsoluteValue) : (0 : AbsoluteValue) + a = a`	стандартные 3
`s1_inverse`	`s1_inverse (a : AbsoluteValue) : a + (-a) = 0`	стандартные 3
`s2_closure`	`s2_closure (a b : AbsoluteValue) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0`	стандартные 3
`s2_mul_associativity`	`s2_mul_associativity (a b c : AbsoluteValue) : (a * b) * c = a * (b * c)`	стандартные 3
`s2_mul_commutativity`	`s2_mul_commutativity (a b : AbsoluteValue) : a * b = b * a`	стандартные 3
`s2_mul_identity_right`	`s2_mul_identity_right (a : AbsoluteValue) : a * 1 = a`	стандартные 3
`s2_mul_identity_left`	`s2_mul_identity_left (a : AbsoluteValue) : (1 : AbsoluteValue) * a = a`	стандартные 3
`s2_mul_inverse`	`s2_mul_inverse (a : AbsoluteValue) (ha : a ≠ 0) : a * a⁻¹ = 1`	стандартные 3
`mul_add_distrib`	`mul_add_distrib (a b c : AbsoluteValue) : a * (b + c) = a * b + a * c`	стандартные 3
`s3_add_assoc`	`s3_add_assoc (r₁ r₂ r₃ : EternalRatio) : (r₁ + r₂) + r₃ = r₁ + (r₂ + r₃)`	стандартные 3
`s3_add_comm`	`s3_add_comm (r₁ r₂ : EternalRatio) : r₁ + r₂ = r₂ + r₁`	стандартные 3
`s3_add_identity`	`s3_add_identity (r : EternalRatio) : r + zero = r`	стандартные 3
`s3_add_inverse`	`s3_add_inverse (r : EternalRatio) : r + (-r) = zero`	стандартные 3
`s3_mul_assoc`	`s3_mul_assoc (r₁ r₂ r₃ : EternalRatio) : (r₁ * r₂) * r₃ = r₁ * (r₂ * r₃)`	стандартные 3
`s3_mul_comm`	`s3_mul_comm (r₁ r₂ : EternalRatio) : r₁ * r₂ = r₂ * r₁`	стандартные 3
`s3_mul_identity`	`s3_mul_identity (r : EternalRatio) : r * unity = r`	стандартные 3
`s3_mul_inverse`	`s3_mul_inverse (r : EternalRatio) (hr : r ≠ zero) : r * r⁻¹ = unity`	стандартные 3
`s3_distributivity`	`s3_distributivity (a b c : EternalRatio) : a * (b + c) = a * b + a * c`	стандартные 3

Семантика вырожденных состояний — 19 теорем, formal/ACT/ExtendedRatio.lean

Поведение finite / infinite / indeterminate: как состояние возникает из деления, как распространяется через сложение и умножение, что делают политики raise/propagate/saturate — и доказательство того, что носитель ExtendedRatio полем не является. Содержательно самостоятельная группа: эти утверждения не переносятся из ℝ, потому что в ℝ таких состояний нет.

Теорема	Формулировка в исходнике	Аксиомы
`fromDivision_of_den_nonzero`	`fromDivision_of_den_nonzero (a b : AbsoluteValue) (hb : b ≠ 0) :`	стандартные 3
`fromDivision_zero_zero`	`fromDivision_zero_zero :`	стандартные 3
`fromDivision_of_num_nonzero_den_zero`	`fromDivision_of_num_nonzero_den_zero (a : AbsoluteValue) (ha : a ≠ 0) :`	стандартные 3
`finite_iff_den_nonzero`	`finite_iff_den_nonzero (a b : AbsoluteValue) :`	стандартные 3
`indeterminate_iff_zero_zero`	`indeterminate_iff_zero_zero (a b : AbsoluteValue) :`	стандартные 3
`add_indeterminate_left`	`add_indeterminate_left (x : ExtendedRatio) : add .indeterminate x = .indeterminate`	стандартные 3
`add_indeterminate_right`	`add_indeterminate_right (x : ExtendedRatio) : add x .indeterminate = .indeterminate`	стандартные 3
`mul_indeterminate_left`	`mul_indeterminate_left (x : ExtendedRatio) : mul .indeterminate x = .indeterminate`	стандартные 3
`mul_indeterminate_right`	`mul_indeterminate_right (x : ExtendedRatio) : mul x .indeterminate = .indeterminate`	стандартные 3
`add_opposite_infinities_indeterminate`	`add_opposite_infinities_indeterminate (d : ExtendedDirection) :`	стандартные 3
`add_same_infinities`	`add_same_infinities (d : ExtendedDirection) : add (.infinite d) (.infinite d) = .infinite d`	стандартные 3
`mul_finite_zero_infinite_indeterminate`	`mul_finite_zero_infinite_indeterminate (d : ExtendedDirection) :`	стандартные 3
`mul_infinite_finite_zero_indeterminate`	`mul_infinite_finite_zero_indeterminate (d : ExtendedDirection) :`	стандартные 3
`saturate_infinite`	`saturate_infinite (d : ExtendedDirection) :`	стандартные 3
`applyPolicy_raise_infinite`	`applyPolicy_raise_infinite (d : ExtendedDirection) :`	стандартные 3
`applyPolicy_raise_indeterminate`	`applyPolicy_raise_indeterminate : applyPolicy .raise .indeterminate = none`	стандартные 3
`applyPolicy_propagate`	`applyPolicy_propagate (x : ExtendedRatio) : applyPolicy .propagate x = some x`	стандартные 3
`applyPolicy_saturate`	`applyPolicy_saturate (x : ExtendedRatio) : applyPolicy .saturate x = some (saturate x)`	стандартные 3
`extendedRatio_not_field_carrier`	`extendedRatio_not_field_carrier :`	стандартные 3

Порядок, метрика, полнота, непрерывность — 18 теорем, formal/ACT/Analysis.lean

Линейный порядок, метрика с неравенством треугольника, полнота пространства и непрерывность сложения и умножения для обоих типов. Как и алгебра, всё это перенесено из ℝ (LinearOrder.lift, MetricSpace.induced): доказано, что перенос корректен, а не то, что модель обладает этими свойствами независимо.

Теорема	Формулировка в исходнике	Аксиомы
`order_reflexive`	`order_reflexive (a : AbsoluteValue) : a ≤ a`	стандартные 3
`order_antisymmetric`	`order_antisymmetric {a b : AbsoluteValue} (hab : a ≤ b) (hba : b ≤ a) : a = b`	стандартные 3
`order_transitive`	`order_transitive {a b c : AbsoluteValue} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c`	стандартные 3
`metric_nonneg`	`metric_nonneg (a b : AbsoluteValue) : 0 ≤ dist a b`	стандартные 3
`metric_symmetry`	`metric_symmetry (a b : AbsoluteValue) : dist a b = dist b a`	стандартные 3
`metric_triangle`	`metric_triangle (a b c : AbsoluteValue) : dist a c ≤ dist a b + dist b c`	стандартные 3
`complete`	`complete : CompleteSpace AbsoluteValue`	стандартные 3
`continuous_add`	`continuous_add : Continuous fun p : AbsoluteValue × AbsoluteValue => p.1 + p.2`	стандартные 3
`continuous_mul`	`continuous_mul : Continuous fun p : AbsoluteValue × AbsoluteValue => p.1 * p.2`	стандартные 3
`order_reflexive`	`order_reflexive (r : EternalRatio) : r ≤ r`	стандартные 3
`order_antisymmetric`	`order_antisymmetric {r s : EternalRatio} (hrs : r ≤ s) (hsr : s ≤ r) : r = s`	стандартные 3
`order_transitive`	`order_transitive {r s t : EternalRatio} (hrs : r ≤ s) (hst : s ≤ t) : r ≤ t`	стандартные 3
`metric_nonneg`	`metric_nonneg (r s : EternalRatio) : 0 ≤ dist r s`	стандартные 3
`metric_symmetry`	`metric_symmetry (r s : EternalRatio) : dist r s = dist s r`	стандартные 3
`metric_triangle`	`metric_triangle (r s t : EternalRatio) : dist r t ≤ dist r s + dist s t`	стандартные 3
`complete`	`complete : CompleteSpace EternalRatio`	стандартные 3
`continuous_add`	`continuous_add : Continuous fun p : EternalRatio × EternalRatio => p.1 + p.2`	стандартные 3
`continuous_mul`	`continuous_mul : Continuous fun p : EternalRatio × EternalRatio => p.1 * p.2`	стандартные 3

Direction · знаковая структура — 3 теорем, formal/ACT/Direction.lean

Инволютивность отрицания, коммутативность и ассоциативность умножения знаков.

Теорема	Формулировка в исходнике	Аксиомы
`negate_involutive`	`negate_involutive (d : Direction) : negate (negate d) = d`	без аксиом
`mul_comm`	`mul_comm (d₁ d₂ : Direction) : mul d₁ d₂ = mul d₂ d₁`	без аксиом
`mul_assoc`	`mul_assoc (d₁ d₂ d₃ : Direction) :`	без аксиом

Как проверить это самому

git clone https://github.com/StudyLabPro/Balansis && cd Balansis/formal
elan toolchain install $(cat lean-toolchain)
lake exe cache get          # готовые .olean Mathlib, иначе сборка займёт часы
lake build BalansisFormal && lake build ACT
lake env lean FormalAudit.lean

# аксиоматическая база конкретной теоремы
echo 'import ACT
#print axioms ACT.a1_exists_unique' > /tmp/axioms.lean
lake env lean /tmp/axioms.lean
# 'ACT.a1_exists_unique' depends on axioms: [propext, Classical.choice, Quot.sound]

Всё, кроме elan и lake exe cache get (это предусловия окружения), выполняет сам генератор аудита — его коды возврата и длительности стоят в таблице выше, а результат целиком лежит в lean-audit.json; сам скрипт — generate-lean-audit.py. Ссылки на исходники на этой странице ведут в коммит 91c406d72421, из которого снят аудит, а не в подвижный master: иначе номера строк разъехались бы молча. README библиотеки, к слову, заявляет меньше, чем доказано: бейдж упоминает только A1–A5, E1–E4 и S1–S3, тогда как семантика ExtendedRatio и весь аналитический слой тоже доказаны. Мы считаем это недоговариванием, а не преувеличением, и поэтому показываем все 73 теорем.