Thanks for the comment! Your reply to an imaginary proof-denier is pretty much what I believe in as well, and it's good practice to always prove things (which was one of the points I tried to make in this blog by the way) and have a certain amount of rigor in how one approaches problem-solving, even as early as the intuiting part of the problem-solving process.

Regarding the point about using "formal proofs" — I am painfully aware of the kinds of images it conjures up. I mentioned Coq and Lean as proof software that could be used to verify proofs, but did not claim that a proof must have that level of rigor. Thanks for pointing that out, and I will try to clear up any misunderstanding that my use of the word "formal" might have brought about.

I used the word "formal" here so extensively just because people on Codeforces seem to call anything they find reasonable a "proof" (an example being the comment you linked to). I wanted to stress the fact that it should be logically sound — in contrast with arguments that people don't even realize have loopholes (like the proof in the linked comment). In fact, even in many editorials while explaining some greedy ideas, people just end up saying "hey, this thing works, and intuition checks out", and people relatively new to competitive programming end up thinking "oh, so this is how a proof works — better think this way the next time I solve a problem".

It's just because of the unfortunate naming used by people that I had to resort to using the word "formal", which is otherwise exclusively used for actual formal proofs that can potentially be unreadable for the uninitiated.

I did link to this webpage, which has some references to how a proof should look like. In the last book they refer to, I believe the concept of a proof is built from the ground up, and it has a simple enough idea of a proof. Again, as I said in the blog too, coming up with a proof once you have basic (correct) intuition pinned down is not hard, and writing proofs gives you unshakeable confidence that what you thought was indeed correct. There is no such thing as a "wrong" "proof" in my opinion — if it is wrong, it is not a proof at all, and logical inconsistencies will eventually show up once you have enough practice. In the way I learned math, I didn't even consider making a wrong argument (of course, there were exceptions, I am not perfect). Maybe I wasn't being creative enough, but I found myself constantly arguing with myself, trying to convince myself that my argument is correct, and completely ignoring the arguments that didn't make sense. In doing so, I found myself going back to a very small set of reasoning methods, which are sort of the foundation of how I reason now. I'm aware that unlearning the pseudo-proof methods that people use right now might be hard for them, and it will take some time to digest the changes (especially because proofs sometimes change how you reason itself, which is a pretty huge change for someone if you ask me).

I also think people should read Everule's blog that you linked. I had a long discussion with him regarding the contents of the blog, and I'd say it mirrors my thoughts on the matter as well.

Very nice proof that sorting is $$$O(n)$$$

Thanks for pointing this out. Honestly, I forgot about that for a bit, because a lot of what I suggested was the opposite of the current trends, and the examples I linked to (that are scattered throughout the text) tell why they need to change.

For instance, there's little rigor in how problems are discussed during the testing phase as well as the proposing phase (especially greedy problems) — people are expected to write only very short proofs, and some negligence creeps in automatically due to the lack of rigor; and editorials are seen as something secondary. The blog claims that the issue lies partly in that and partly in not seeing testing from a security-based perspective, and it is only by making changes to this perspective on problem-setting that mistakes can be avoided.

More specifically:

• Current trends in problem-setting are "intuitionist" (I know I am using that word wrongly) and focused on being fast, rather than built on being precise.
• They are bad because they lead to mistakes even in things as fundamental as intended solutions, which is something unthinkable in other types of contests (like most respectable mathematical Olympiads).
• They should go towards what I mentioned in the blog. Or at least they can take some pointers from the suggestions made in the blog, which have given me some success in making the coordination process easier and contests less error-prone.

One example is this: in a game theory problem in a contest I coordinated, there was a DP to find winning and losing states. The intended constraints were such that a linear/linearithmic solution passes. However, it turned out that you could tweak the order of computing some things in a brute-force solution to get an $$$O(n \log n)$$$ algorithm, by just doing $$$O(n / i)$$$ operations for the $$$i$$$-th step.

Tweaking just the order is what I call a heuristic here (it's quite simple to mindlessly guess that it will work), and often there are situations where these kinds of heuristics come up and have provably good properties.

While it is not proven, it is a heuristic. When it is proven, it is an algorithm.
Similar to how a proven hypothesis is a theorem.