Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

▲

impendia 17 hours ago | parent | next [-]

> Are you an expert?

I can't speak for ndriscoll, but I am a university math professor with extensive experience teaching these sorts of topics, and I agree with their comment in full.

You are right that some (other) statements are harder to formalize than they look. The Four Color Theorem from graph theory is an example. Generally speaking, discrete math, inequalities, for all/there exists, etc. are all easy to formalize. Anything involving geometry or topology is liable to be harder. For example, the Jordan curve theorem states that "any plane simple closed curve divides the plane into two regions, the interior and the exterior". As anyone who has slogged through an intro topology book knows, statements like this take more work to make precise (and still more to prove).

	▲	11 hours ago \| parent [-]
		[deleted]

▲

codeflo 19 hours ago | parent | prev | next [-]

> apparently

When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.

▲

freehorse 16 hours ago | parent | next [-]

To be fair, the comment did not explain any concept that I can see, or why this statement is simple. It gave the statement and said it was simple to formalise. It does seem simple enough to me (basic arithmetic statement with a few variables and a bunch of quantifiers) but if somebody has no expertise/intuition, I think it is a fair question, without any hostile intent assumed.

▲

IsTom 18 hours ago | parent | prev | next [-]

> it's rare that the theorem statement itself is particularly hard to formalize

That's very dependent on the problem area. For example there's a gap between high school explanation of central limit theorem and actual formalization of it. And when dealing with turing machines sometimes you'll say that something grows e.g. Omega(n), but what happens is that there's some subsequence of inputs for which it does. Generally for complexity theory plain-language explanations can be very vague, because of how insensitive the theory is to small changes and you need to operate on a higher level of abstraction to have a chance to explain a proof in reasonable time.

	▲	zozbot234 16 hours ago \| parent [-]
		Yes, if the theorem statement itself is "hard to formalize" even given our current tools, formal foundations etc. for this task, this suggests that the underlying math itself is still half-baked in some sense, and could be improved to better capture the concepts we're interested in. Much of analysis-heavy math is in that boat at present, compared to algebra.

▲

kelipso 13 hours ago | parent | prev | next [-]

Lol it’s weird seeing high school redditors saying gatekeeping and are you an expert in the same thread as university professors, all talking about the same topic. But I guess that’s HN for you.

▲

phyzome 15 hours ago | parent | prev [-]

I think it was a fine question to ask in the context of a discussion of epistemology.

▲

tetha 14 hours ago | parent | prev | next [-]

As the sibling comment says, in my experience, the difficulty of formalizing the problem varies greatly between different areas. Probability theory is another notorious field in which modelling a problem correctly can be very subtle and difficult.

On the other hand, many problems in number theory and discrete structures tend to be rather simple to formalize. If you want to take your own look at that, I'd recommend to check out the lean games[1]. I'd say after the natural numbers game, you most likely know enough lean to write that problem down in lean with the "sufficiently small" being the trickiest part.

1: https://adam.math.hhu.de/

▲

dooglius 21 hours ago | parent | prev | next [-]

I think you may be confusing specification of the problem and the formalization of the proof.

▲

21 hours ago | parent | prev | next [-]

[deleted]

▲

schrodinger 10 hours ago | parent | prev [-]

Voters: please reconsider your ups and downs. I think the “Are you an expert” question triggered a lot of downvotes when it was in fact asked in good faith to judge the person’s perspective of easy and hard.

▲

NetMageSCW 8 hours ago | parent [-]

And I would say there is no way to ask that question in good faith. (Tedious proof by cases left as an exercise for readers.)

The correct question would have been, does anyone else agree with the statement.

In this particular case, the amount knowledge needed (of e.g. Lean language, math and Erdos problems) means any credible statement about the difficulty requires an expert.

	▲	oh_my_goodness an hour ago \| parent [-]
		"Are you an expert?" is a perfectly respectful question.