Search results

the strength of the zero product property

Status: Open.

#5315 In metamath/set.mm;

· jkingdon opened on May 29, 2026

The set of bags dominated by a given bag is finite

Status: Open.

#5310 In metamath/set.mm;

· jkingdon opened on May 26, 2026

Determine when avoiding derived axioms should count as axiom saves

Status: Open.

#5227 In metamath/set.mm;

· BTernaryTau opened on Mar 12, 2026

Reorganize the sections about finite intervals of integers

Status: Open.

#5178 In metamath/set.mm;

· ProgramCrafter opened on Jan 25, 2026

Citing Lean proofs

Status: Open.

#5138 In metamath/set.mm;

· sctfn opened on Dec 13, 2025

Make an extensible structure a map from small integers to sets (Dec 2025 version)

Status: Open.

#5136 In metamath/set.mm;

· jkingdon opened on Dec 9, 2025

update mm100

Status: Open.

#5126 In metamath/set.mm;

· icecream17 opened on Nov 30, 2025

Update conventions re: tags

Status: Open.

#5125 In metamath/set.mm;

· icecream17 opened on Nov 27, 2025

checkmm.cpp test not failing

Status: Open.

#5107 In metamath/set.mm;

· sctfn opened on Nov 16, 2025

The fundamental theorem of Galois Theory

Status: Open.

#5106 In metamath/set.mm;

· tirix opened on Nov 16, 2025

Rules for adding theorems to the main part of set.mm

Status: Open.

#5064 In metamath/set.mm;

· avekens opened on Oct 19, 2025

Translating Deepmind's formal conjecture collection to Metamath?

Status: Open.

#4994 In metamath/set.mm;

· ghost opened on Aug 27, 2025