Also, the fact of faking a terror attack and everybody just shrugging it off as an obvious Russian false flag op. I think even Orbán understood at that point that the jig was up.
One thing that's surprised me over the last few years is how much Russia messes with global politics. It seems to seeping into public consciousness so instead of being seen as a bit of a conspiracy theory you now have the crowds shouting Russia out. I don't know if that'll effect other Russia backed projects like Brexit financed by Russia via Arron Banks and Trump, financed by the "We have all the funding we need out of Russia" stuff. It doesn't seem illegal but the voters may be getting fed up with it all?
It's worth noting that the party vote share here was 53% for Tisza vs. 44% for the even-more-right-wing parties. The fact that this results in a two thirds majority is because the electoral system inflates the strongest party. Orbán has previously achieved two thirds majorities multiple times while winning less than 50% of the party vote. Most seats are assigned not through party lists but in single-member constituencies with first-past-the-post voting, same as in America. So it's not "convince two thirds of the people to vote for you", it's "convince a very slim plurality in two thirds of the constituencies to vote for you".
I'd like that. But this system is very attractive for the strongest party, so it will be a real test of their commitment to actually representative, multi-party democracy. Also, the general system (a mix of single-member constituencies and party list seats, with more of the former than the latter) isn't a Fidesz invention, it has a long legal tradition in Hungary. So there might be a lot of resistance to a purer party-list system on those grounds too.
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.
It's a bit like computer security: you have to get it right all of the time and the perps mostly only need one shot at being lucky and then it will takes many years to undo the damage.
We should approach democracy more with the kind of insight that go into making computers secure. Oh, wait...
Oooh, bikeshedding! To me your `import math with x as y` reads like "import all of math, making all of its symbols visible, just renaming some of them". That's different from the intended "from math, import only x (maybe with a renaming)".
This is someone's private project for their own amusement. It's clearly not in a state where it would be "useful" to "users". Nor is it meant to be. At the moment it's meant for compiler geeks to look at.
Not every readme is a sales pitch for Enterprise Quality(tm) software.
> It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
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.
>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?
Yes, I agree! My issue is not with the reality of having reduced the problem to a different one, but with the "goal" metaphor, which is counterintuitive to how that term is normally used, especially since it connotes that each step is some brand new thing, rather than progress.
And sure, like any technical jargon, you can learn to accept some specialized term-of-art usage, but I'd prefer it be conducive to developing a correct ontology of what is going on in an assisted Lean proof.
While "subgoal" is better, I think the issue even goes back to calling the original theorem a "goal". Really, the goal is to prove the theorem. So a better term, more conducive to intuiting the Lean ontology, would be something like "[remaining] unresolved proof state", even though it's more verbose. (Perhaps you could get the best of both worlds with some kind of footnote for new users that clarifies that this is what "goal" means here.)
With that said, I appreciate the pushback, as your comment forced me to more carefully think about what I was objecting to.
Gotcha. I've never had a problem with this usage. I guess I see the objection of "the goal is to prove the theorem" vs. "the (initial) goal is the theorem". It strikes me as overly pedantic, but we're talking about formal methods, so I guess pedanticism is warranted.
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.
Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.)
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)
Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.
Fair! I decided not to do that because the way arguments work (and dependent types in general — like being able to return a proof of `x = x` given x) is unusual for people like me, and deserves an article of its own. So I’m kicking that to one of the next articles.
Rocq used to have a "mathematical proof language". It's hard to find examples, but this shows the flavor (https://stackoverflow.com/a/40739190):
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.
So the idea was to make proofs read more like "manual" proofs as you would find them in math papers. Apparently nobody used this, so it was removed.
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
You spell out the structure and intermediate results you want, and the "by ..." blocks allow you to specify concrete tactics for parts where the detains don't matter and the tactic does what you want. In this proof, "simp" (a kind of simplify/reflexivity tactic) is enough for all the intermediate steps.
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.
You can structure your proofs in Lean to reason forward, but proofs in Mathlib still primarily do backward proof, because it is more compact and performant.
Declarative proof languages support backward proof, typically phrased as: "suffices <statement> by ... " i.e. it suffices to show <statement>, and the current goal follows.
Yes, there is a prelude that defines natural numbers and an addition function on them. As the post notes, the reflexivity tactic "unfolds" the addition, meaning that it applies the addition function to the constants it is given, to arrive at a constant. This is not specific to addition, it unfolds other function definitions too. So addition doesn't have to come first, you are right that reflexivity is more fundamental.
Author here — this is correct. I’ve added a paragraph on this in an edit btw so it’s possible the parent poster hasn’t seen it yet. Reproducing the paragraph:
(Here, rfl closes ⊢ 3 + 3 = 6, but for a different reason than one might think. It doesn’t really “know” that 3 + 3 is 6. Rather, rfl unfolds the definitions on both sides before comparing them. As 3, 6, and + get unfolded, both sides turn into something like Nat.zero.succ.succ.succ.succ.succ.succ. That’s why it actually is a something = something situation, and rfl is able to close it.)
reply