# | User | Rating |
---|---|---|
1 | tourist | 3985 |
2 | jiangly | 3741 |
3 | jqdai0815 | 3682 |
4 | Benq | 3529 |
5 | orzdevinwang | 3526 |
6 | ksun48 | 3489 |
7 | Radewoosh | 3483 |
8 | Kevin114514 | 3442 |
9 | ecnerwala | 3392 |
9 | Um_nik | 3392 |
# | User | Contrib. |
---|---|---|
1 | cry | 166 |
2 | atcoder_official | 163 |
3 | Um_nik | 162 |
3 | maomao90 | 162 |
5 | adamant | 157 |
5 | -is-this-fft- | 157 |
5 | djm03178 | 157 |
8 | awoo | 155 |
9 | TheScrasse | 154 |
10 | Dominater069 | 153 |
Name |
---|
orz blog
Coincidence? I think not
I think that your blogs produce the opposite effect of what you are trying to achieve (although my skill for understanding people is negative, so take that with a grain of salt).
You make it seem that proving is something hard that is only available to people with special education in math. You insist on using the phrase "formal proof" which seems to suggest writing everything in symbols, maybe even starting proving from axioms. You mention Coq, and as a person who had a course in Coq and remembers how hard it is to prove "obvious" stuff like the commutativity of addition for integers, I can say that it is not good for supporting your position.
From here I will address an imaginary
flat-eartherproof-denier.Mathematical proof is an argument so convincing, that you are prepared to use it to convince other people. Imagine a person who doesn't believe in your claims (imagine me). But they don't want to mess with you, they want to get convinced, they just don't want to trust your word. Can they find a hole in your arguments? If not, it is strict.
It's ok to use natural language in proofs. It's ok to reuse known theorems in proofs. It's ok to cut some corners (but only after you got some experience). It's ok to say that something is obvious.
It's not ok to believe in some greedy and justify it by saying "it's clear that this is the worst case and we are doing fine in it". Because there are very few situations when you can actually understand what is the worst case for your greedy.
Here is the example of "your average it's the worst case logic": A decreasing array is clearly the hardest to sort in increasing order, it even has the maximum number of inversions. A decreasing array is sorted by reversing the array. Therefore, reversing the array sorts the array in $$$O(n)$$$.
Ridiculous? But how is it different from this?
There shouldn't be any assumptions in your proof, apart from the ones given in the statement. There are some quasi-exceptions to this, like if the problem has random input, it's ok to say that some property will hold because of randomness and then just check that it actually holds by running the code a lot of times. Or something similar. Running an exhaustive search is a valid method of proving. Running your greedy on some tests you believe to be the worst is not.
Read Everule's blog and comment section. Try to come up with proofs yourself. You will get better with practice.
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.
Yes, that's why I wrote the first part of the comment. I understand that you are working for a good cause, but I feel like you are presenting your position in an unflattering light, thus harming the position in eyes of the reading public. So I wanted to nudge you into revising it :)
Yes, the language is flawed. The things people call proof sometimes drive me crazy. But we need to break the wall of supposed superiority and scary-sounding words.
I actually don't like the link to AoPS you provided, because the text on the page is reinforcing the image that proofs should be maximally pedantic and they are for mathematicians only:
Then they mention proof by construction and proof by contradiction, which are much better, but they don't say that the two-column format is unnecessarily rigid and don't expand on two actually nice proof types.
Somewhere around 7-8th year in school (11th year is senior year, for context) I read a book called "Geometry for dummies" or smth, which introduced two-column proofs to me. I started writing my proofs on geometry lessons in the very strict two-column style. Simple problems on 3-4 lines took me a couple of pages. After a week the teacher asked me to stop.
Even more, in the next paragraph they say
directly comparing informal proofs to two-column proofs for some reason. Then
Which reads as "we, real mathematicians, do not stoop to your informal level, it is for children". And since directly opposing informal proofs we have two-column proofs, it implies that two-column proofs are the right way to go.
They don't say anything negative about two-column proofs. You need to use hyperlinks twice to get here and see
Then there are links to articles and a book you can buy on Amazon (thanks?). I opened the links, but the articles are pretty long, even I haven't read them yet (although they are still open in my browser and I want to read them later), the person who doesn't believe in proofs will just close it right away even if they decided to click, which is already much more effort than we should expect.
Regarding your first point: I did intentionally post this slightly controversial (but honest) opinion just to get the ball rolling, and I agree that the main issue is people being scared of proofs, so that wasn't really the right approach here. Maybe I'll make up for it by adding a link to the blog you mentioned, and some of the things on proof writing that I myself read (and not second-hand advice, like the AoPS page).
I should have been more alert in pursuing an explanation of what proofs are, that's my bad. I just linked the page because (I thought) I saw an explanation of how usual proofs are different from formal proofs, and the reference had a nice book.
The book mentioned is available for free online (on a course webpage, so I think it should be fine), and I highly recommend going through at least the chapter on proofs, if you don't want to learn about everything else.
I tend to find myself trying to wrap my head around how some people can so confidently assert some claims that are completely false, and how they continue to believe in flawed reasoning even after it is pointed out to them. Maybe it's because I have a math Olympiad background, which had a very strong focus on proofs, compared to competitive programming, where people think programming is more important. I tried finding resources on proofs that I used, but unfortunately, I couldn't find any. Perhaps practice with mathematical arguments is the only thing that teaches you to reason confidently.
Very nice proof that sorting is $$$O(n)$$$
Your blog has "why problemsetting trends need to change" in the title but I don't understand what your blog has to do with this. As far as I can tell, your blog is mostly about "things that you should do when preparing a problem for a contest" but doesn't discuss what current trends are, why current trends are bad, or where you think they should go.
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:
How do we really "prove" whether a heuristic works correctly and fast enough? If it could be proven to be correct, then should it be called a heuristic, rather than an "algorithm"? Say, someone has a heuristic improvement to a problem. Maybe, someone claims that using the infamous "dancing links" technique on a sudoku solver can improve the asymptotic time complexity over the usual backtracking solution. Or probably, they claim that the Simplex algorithm is faster than Interior-point methods in practice, but the worst-case analysis tells them otherwise. How will we prove/disprove these kind of claims?
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.