SkidanovAlex

It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct.

This is how the theorem for FLT looks in the particular proof we discuss here:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct.

This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof.

(Not impossible: such a bug indeed was recently discovered (and patched))

Given your description, it is very likely that you actually only completed the act 1 of the game. The "jump scare" is not the end.

Isn't the first example (with the cartoon) in text mode?

The most important aspect of blockchain that is relevant here is that your counterparty half a world away and you both agree that you trust the state of this blockchain, and thus can transact on it.

For business running the same code on their 1 node instead of N is not a replacement, because their counterparty has no reason to trust whatever is running on that 1 node.

Your reasoning re: N nodes are expensive is also flawed. Executing a single payment transaction takes a fraction of a second of compute. Even if it is replicated 10,000X, it's still extremely cheap compute-wise. The low cost of transactions has nothing to do with subsidizing.

MS Paint though is "either real or a Good Clone :)", because you can zoom to 12x by clicking one-pixel-wide line below 8x.

While I believe that the city should share the schema, and that the city is effectively argues for security through obscurity, I disagree with the main premise of the article: that knowing SQL schema doesn't help the attacker.

If I understand the argument of the author here:

> Attackers like me use SQL injection attacks to recover SQL schemas. The schema is the product of an attack, not one of its predicates

The author appears to imply that once the vulnerability is found, the schema can be recovered anyway. It is not always the case. It is perfectly viable to find a SQL injection that would allow to fetch some data from the table that is being queried, but not from any other table, including `information_schema` or similar. If all the signal you get from the vunlerability is also "query failed" or "query succeeded, here's the data", knowing the schema makes it much easier to exploit.

> the problem is that every computer system connected to the Internet is being attacked every minute of every day

If you specifically log failed DB queries, than for all the possible injections that such 24/7 attacks would find you have already patched them. The log would then be not deafening until someone stumbles on the actual injection (that, for example, only exists for logged in users, and thus is not found by bots), in which case you have time to see it and patch before the attacker finds a way to actually utilize it.

Knowing schema both expedites their ability to take advantage of the vulnerability, but also increases their chances of probing the injection without triggering the query failure to begin with.

Would help a lot if somewhere at the very top it explained what tree calculus is (may be extend the animation of the addition example to first show what the t is)

It took me a while on the website to understand what it was all about. As it is it looks more like a website for a functional programming language.

There's an outstanding episode of Black Mirror called Crocodile, that explores this idea.

USS Calister is also a very good episode with the same premise.

Watch Black Mirror episode called Metalhead.

Who decides that the videos in Russia are factual, while the videos in the US are not?