[hansvm]

Hahaha, I know what you mean.

It's been awhile since I've looked at NSA on graphs, but it's an interesting field of study. For something of a taste, an alternative proof of Kőnig's lemma might look like:

- Start with a locally finite, connected, infinite graph G.

- Choose any nonstandard extension G* of G.

- By the transfer principle (basically just logical compactness), there exist hyperpaths [0] of unbounded (hypernatural) length in G*. Pick one, P*.

- Restricting P* to G you obtain some path P, which is the infinite path you're looking for.

I settled into industry instead, but that's the sort of thing I'd like to study if I ever go back for a PhD, hence the interest in those sorts of ideas applying to spectral theory.

[0] The "transfer" of a path isn't actually necessarily a connected path in the usual sense, but it's indexed by the hypernaturals, and each well-ordered countable segment is connected. I'm skipping the entire intro that makes those operations make sense.

[klyrs]

Dammit, I had hoped I'd nerdsniped you... but the nerdsniper is you and now I'm curious!

[hansvm]

Well, you did nerdsnipe me too :) I haven't looked at this in awhile, and my curiosity is re-ignited.

The most basic style of proof in a lot of nonstandard analysis is (1) lift your problem to a nonstandard space, (2) prove something interesting in that space, (3) hopefully project something interesting back down to the problem you actually care about.

E.g., in nonstandard real analysis you can look at a real-valued function like f(x) = x^2, pick any epsilon z, and compute the hyperreal analogue (f(x+z)-f(x))/z = 2x + z. This is within some infinitesimal of 2x, so you use some machinery you've built up to conclude the derivative of the real-valued function is 2x.

The graph lemma above had a similar flow. Create G*, find something interesting, project it back down to G, finish the proof.

That's certainly not the only proof style. Nonstandard topology combines basically all the normal compaction theorems into one, for example, and that's a bit more intricate.

Even such crude techniques can bear fruit quickly though. Menger's theorem was proven in the early 1900s, and only extended to infinite graphs in the late 1900s. That 3-step proof process with nonstandard graphs makes it a bog-standard freshman exercise for locally finite infinite graphs, and only a bit more involved for the full generality originally proven by Erdos and friends.

I don't have any deep insights beyond that. The Springer GTM series has a nice intro to nonstandard analysis (not actually graduate-level IMO, a mid/advanced undergrad could use it, which is a nice level for that sort of book), building it up in a way that you could probably work with nonstandard extensions of other infinite structures (like graphs) without needing many/any other resources, especially if you've done much with building models of other theories via set structures.

[klyrs]

> (3) hopefully project something interesting back down to the problem you actually care about.

Indeed, and this is the step that standard mathematicians tend to balk at.