Issues

• Polynomials with no variables (iset.mm)

  metamath/set.mm#5539 · Filter by author jkingdon opened on Oct 15, 2026
  2

• "scalar product" --> "scalar multiplication"

  metamath/set.mm#5512 · Filter by author icecream17 opened on Sep 28, 2026
  2

• FLT for n = 3

  metamath/set.mm#5508 · Filter by author avekens opened on Sep 26, 2026
  1

• Fermat's Last Theorem (metamath 100 #33)

  metamath 100
  metamath/set.mm#5507 · Filter by author avekens opened on Sep 26, 2026
  5

• Clearer documentation on how to get started

  metamath/set.mm#5485 · Filter by author jkingdon opened on Sep 10, 2026
  2

• Multi-file transition: Tool Readiness

  metamath/set.mm#5478 · Filter by author tirix opened on Sep 5, 2026
  15

• Tree and spanning-tree foundations toward Euler's formula

  metamath/set.mm#5435 · Filter by author mountain opened on Aug 14, 2026
  4

• Convert Euclidean n-spaces to 0-based indices

  metamath/set.mm#5416 · Filter by author tirix opened on Jul 29, 2026
  17

• Transformation of JM's mathbox

  metamath/set.mm#5412 · Filter by author avekens opened on Jul 26, 2026
  4

  

• Indicate when a proof is automatically generated

  metamath/set.mm#5379 · Filter by author BTernaryTau opened on Jul 12, 2026
  16

• Determine when avoiding derived axioms should count as axiom saves

  metamath/set.mm#5227 · Filter by author BTernaryTau opened on Mar 12, 2026
  7

• Reorganize the sections about finite intervals of integers

  metamath/set.mm#5178 · Filter by author ProgramCrafter opened on Jan 25, 2026

• Citing Lean proofs

  metamath/set.mm#5138 · Filter by author sctfn opened on Dec 13, 2025
  3

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

  metamath/set.mm#5136 · Filter by author jkingdon opened on Dec 9, 2025
  2

• update mm100

  metamath/set.mm#5126 · Filter by author icecream17 opened on Nov 30, 2025
  7

• Update conventions re: tags

  metamath/set.mm#5125 · Filter by author icecream17 opened on Nov 27, 2025
  4

• checkmm.cpp test not failing

  metamath/set.mm#5107 · Filter by author sctfn opened on Nov 16, 2025
  2

• The fundamental theorem of Galois Theory

  metamath/set.mm#5106 · Filter by author tirix opened on Nov 16, 2025
  15

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

  metamath/set.mm#5064 · Filter by author avekens opened on Oct 19, 2025
  7

• Translating Deepmind's formal conjecture collection to Metamath?

  metamath/set.mm#4994 · Filter by author ghost opened on Aug 27, 2025
  2

• Changing requirements for "definitions"

  metamath/set.mm#4955 · Filter by author benjub opened on Aug 1, 2025
  64

• Problem with $j tags

  metamath/set.mm#4951 · Filter by author wlammen opened on Jul 30, 2025
  8

• Intermediate value theorem is equivalent to (some constructive taboo)

  metamath/set.mm#4918 · Filter by author jkingdon opened on Jun 29, 2025
  12

• Inconsistency ?

  metamath/set.mm#4904 · Filter by author tirix opened on Jun 20, 2025
  2

• Status of syl related renames

  metamath/set.mm#4902 · Filter by author jkingdon opened on Jun 19, 2025
  2