Search results

Project: eliminate axiom of choice usage in ~friendship

Status: Open.

#5181 In metamath/set.mm;

· ProgramCrafter opened on Jan 26, 2026

Reorganize the sections about finite intervals of integers

Status: Open.

#5178 In metamath/set.mm;

· ProgramCrafter opened on Jan 25, 2026

Revise division label

Status: Open.

#5176 In metamath/set.mm;

· icecream17 opened on Jan 22, 2026

What's the easiest way to show that the power set of a singleton is not infinite? (iset.mm)

Status: Open.

#5156 In metamath/set.mm;

· jkingdon opened on Jan 4, 2026

Citing Lean proofs

Status: Open.

#5138 In metamath/set.mm;

· sctfn opened on Dec 13, 2025

Dependently typed induction (or recursion) principle

Status: Open.

#5137 In metamath/set.mm;

· jkingdon 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