> This is quite immature.

For research math, it is "immature",
incomplete, .... But I was aiming the
remark at students plus/minus a few years
of being a college freshman.

For what theorems to prove:

(1) "Alexander Grothendieck, who spoke of
tackling hard problems by creating a
gradually rising sea of ideas around
them."

https://www.quantamagazine.org/monumental-proof-settles-geom...

(2) Something missing: As a grad student
studying the Kuhn-Tucker (KT) conditions
and the constraint qualifications (CQ),
there was interest in implications among
the CQs. Two of the famous CQ were (a)
the Zangwill and the (b) KT, but the
implications between them were "missing".
So, that was a problem, a theorem "need to
prove". My approach was to look for a
counterexample among wildly goofy sets,
e.g., the Mandelbrot set or Brownian
motion. As appropriate for the KT work,
both sets were closed. Hmm .... So,
needed an optimization objective
function to be minimized. So, ..., soon
enough, for each closed set there is a
real valued function zero on the closed
set, strictly positive otherwise, and
infinitely differentiable. Then I had a
counter example. Two weeks of work in a
reading course. Published it.

Was doing some AI for monitoring but
wanted a better approach, the "need".
Used the probabilistic concept tightness
to get another approach, the basis of the
"proof", widely applicable because still
distribution free (i.e., made no
assumptions about probability
distributions, e.g., Gaussian). Published
it.

(3) A problem from outside math: As in

https://news.ycombinator.com/item?id=40893566

the FedEx BoD wanted some revenue
projections, wanted so much it nearly
killed FedEx. So, as in that Hacker News
URL, got some "intuition", ..., got a
simple differential equation (the
theorem), solved that (the proof).

Currently my startup needed some progress,
and I formulated a suitable theorem and
proved it.

A concern about such theorems and proofs,
for the published ones, the check has yet
to arrive.

Was eating lunch with some well known
mathematicians, and they asked what I was
working on. I explained, "scheduling the
fleet at FedEx, which airplanes go to what
cities in what order". Immediately one of
the mathematicians with contempt scoffed
and said "the traveling salesman problem"
as if that was the "theorem" to be proved,
i.e., P = NP.

Nope: I was just trying to save FedEx
some money. So, my approach was 0-1
integer linear programming (ILP) set
covering; that this is in
NP-Complete was to me next to irrelevant; I
just wanted feasible solutions that would
save money. Maybe over a year the savings
would be some $millions, but each feasible
solution might be $1000 above an optimal
solution. At 365 days a year, I'd leave
$365,000 on the table. Fine with me!!!
To the mathematician, all that
consideration of money was irrelevant --
he wanted to focus on P = NP and regarded
that as too difficult (it still is) and I
was foolish for working on it (I wasn't
working on it). In short I was counting
the millions to be saved, not the
thousands of saving to be missed.

Later there was a 0-1 ILP with 40,000
constraints and 600,000 variables. I used
the IBM OSL (Optimization Subroutine
Library) and in 900 primal-dual iteration
for Lagrangian relaxation got a feasible
solution within 0.025% of optimality.

Lesson: O-1 ILP can be a good tool in
practice, sometimes can save a lot of
money.

So the well-known mathematician and I
disagreed on your "which theorems you need
to prove"!!!

Of course there is the now famous

Garey and Johnson, Computers, and
Intractability, Bell Labs, 1979.

The authors were trying to find a least
cost design for some Bell network.

On pages 2-3 we see some cartoons with

"I can't find an efficient algorithm, I
guess I'm just too dumb."

and

"I can't find an efficient algorithm, but
neither can all these famous people."

It turns out by "an efficient algorithm"
they meant (a) getting least cost
solutions, least down to the last tiny
fraction of a penny, (b) to worst case
problems, (c) guaranteed, (d) with
computer time growing no faster than some
polynomial in the size of the problem.

I just wanted to save FedEx some $millions
a year.

The famous mathematician insisted on
(a)-(d) or no savings at all.