• CanadaPlus@lemmy.sdf.org
      link
      fedilink
      arrow-up
      4
      ·
      edit-2
      6 months ago

      So don’t use it in non-KRY-definite AA situations, or you could get erroneous results. QQX is fine though, as long as you have non-vanishing ABCD. /s

      I wonder if Lean proofs become the new peer review like I’ve heard suggested, if mathematics might break from this, and look more compsci-ish in the future. That way non-specialists could get up to speed quickly.