Obvious tweaks exist, of course: Even if you keep more individual constituencies than party list seats, they should use some sort of instant runoff/ranked choice/etc. system. But other first past the post countries are dragging their feet on this too, so... we'll see.

Not every readme is a sales pitch for Enterprise Quality(tm) software.

I do want to note that systems usually use terms like "current goal" or "active goal", which do imply a sense of progress. I never felt that they imply that the current goal is a brand-new thing. It's a transformed version of the previous goal, hopefully made up of simpler parts that eventually become so simple as to be trivial, which then completes the overall proof.

Interesting. Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work? And if we then do brush our teeth, wouldn't you say that the remaining goal is to get to work? In this scenario, if anything can be called progress, it is what's in the past (the showering etc.), not what is still to be done.

I would find the following a more convincing presentation:

    theorem x_eq_x (x:nat) : x = x := by
      rfl

    theorem 2_eq_2 : 2 = 2 := by
      exact (x_eq_x 2)

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.

Isabelle's Isar proof language is similar, and AFAIK the standard way of proving in Isabelle (example from https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-...):

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed

I don't know if there is anything like this for Lean, but maybe this provides some keywords for a web search. Or inspiration for a post in some Lean forum.

And yes, this means that many laypeople are not effective at doing mathematics. Does this surprise you? If yes, then the linked article and Mastodon thread may be interesting to you. Which is why I submitted them.