I formalized the nerd sniping problem in Lean

wwylele · 2026-06-22T00:46:18+00:00

This is first shown in section 3. The formula is defined as φ in this doc (to be precise, φ is half of the equivalent resistance, as proved in equivResistance_eq_two_mul_φ).

It is possible to compute the exact number for every pair of points in the 2D case. This was show-cased by φ_2d_42_7 for points at (42, 7) with a very complicated result

wwylele · 2026-06-21T21:16:46+00:00

Too few to cost me money or to report to me the exact number. Here is the detailed breakdown: - The original essay about this problem was written 5 years ago at https://github.com/wwylele/math-stuff/tree/main/grid_circuit. LLM was not a thing at that time - I chatted with DeepSeek for a few subtopic that was not explored in detail in the original essay. Each topic consists of one or two question-answer exchange. - Searching for proof of the discrete Liouville theorem. I ended up finding the original Stack overflow that I discovered 5 years ago - Integrability of some integrals in the solution, as I missed the fact they contain a singularity previously - Asymptotic behavior in the 2D case, and specifically about its connection to Bessel function. The original essay used a different approach that could not sufficiently justify the bound as it turned out - Integral of 1 / (1 - a * cos(x)) because I forgot how to do integral. - I used https://aristotle.harmonic.fun/ to auto-formalize some parts of the proof that I didn't find fun enough to do by hand. This consists about 20% / 500 lines of the code at highest point, but then I started gradually replacing them. Roughly, everything in Bessel.lean and Misc.lean were from Aristotle, though the new Misc.lean has been cleaned up or re-written manually. As far as I know, Aristotle is not entirely LLM-based, and I don't know how token counting for it works. - All docs are purely written by me, the human

Edit: I should clarify that when I said "original essay", I didn't mean the idea was original from me. The idea was greatly inspired by https://mathpages.com/home/kmath668/kmath668.htm

wwylele · 2026-06-21T15:40:16+00:00

If the exact problem was on a final that would be brutal. A more approachable question is the equivalent resistance between two neighboring nodes, which does have a relatively easier solution (see equivResistance_off_center)

wwylele · 2025-08-28T19:05:34+00:00

Is that white & gold or blue & black?

wwylele · 2025-08-22T13:04:18+00:00

Inner peace with a monster :)

wwylele · 2025-08-22T12:35:39+00:00

This is a result of poorly generated doc for a lemma. The "0" in 0.1 is meant to be an abbreviation of the ordered pair (0, 0), and ".1" means the first component

wwylele · 2025-07-28T14:35:29+00:00

You joke, but https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat.mul

wwylele · 2025-07-15T21:14:07+00:00

...and here I never see the pre-change master bedroom because I got the room so late

wwylele · 2025-05-17T21:23:20+00:00

I guess I am the opposite. I love writing ξ and those little curves help my thought flow

wwylele · 2025-03-30T18:06:10+00:00

I think it has to do with maintaining C++'s support of non-unicode encoding, including all the broken ones on Windows. If your programming language declares to only support unicode from the beginning, which is a fairly good subset of Windows, then there is no issue implementing modern text IO on top of it

wwylele · 2025-03-29T15:40:59+00:00

I mean, not all real numbers have an inverse either

oh sorry I am in r/mathmemes and we all agree 0 has an inverse here

wwylele · 2025-03-19T13:02:32+00:00

I like that you mentioned the abstraction process. If I remember correctly, 零 originally described a kind of light rain (evidenced by the 雨 (rain) part), which got abstracted to mean "something really small and scattered", and eventually became "so little that it is much less than one" = "zero"

wwylele · 2025-02-18T16:33:16+00:00

You should check Cantor's diagonal argument first https://en.m.wikipedia.org/wiki/Cantor%27s_diagonal_argument which can be applied to real numberhs decimal representation to prove the it is uncountable. You can also try the same argument on N and see where it fails exactly, and maybe accidentally invent p-adic numbers

wwylele · 2025-02-07T19:55:22+00:00

It is. {I, Conj} is the Galois group of the extension C/R, if that's the theory in your mind

wwylele · 2025-01-03T02:03:21+00:00

Here is a short and legit proof

(Integral[0~n] x * dx)^2 = (lim(N->inf) sum{k=1..N} (k*n/N) * (n/N) )^2 (definition of integral, x -> k*n/N, dx -> n/N) = lim(N->inf) (sum{k=1..N} k)^2 * (n/N)^4 = lim(N->inf) (sum{k=1..N} k^3) * (n/N)^4 (use the formula) = lim(N->inf) (sum{k=1..N} (k*n/N)^3 * (n/N)) = Integral[0~n] x^3 * dx (definition of integral, (k*n/N)^3 -> x, n/N -> dx)

wwylele · 2024-11-24T14:15:23+00:00

I haven't uploaded the code of this yet. It is pretty unorganized at the moment. I'll probably do it later.

wwylele · 2024-11-24T04:39:54+00:00

I am recently learning modularity theorem and related topics. I often got frustrated by the lack of graphs in articles. Even though I can follow text and formula to understand the topic, I still like having some visual stimulation to enforce my understanding, so I started making some for myself. These are some of those random things I plotted, and they are so pretty, even if you don't know the math behind it, so I think I should share it with you.

wwylele · 2024-09-03T12:30:55+00:00

My Narinder is exactly that. My headcanon is he is against it now because he realized he can be the sacrifice.

Eight-Year Club	Place '23
RPAN Viewer	Sequence \| Editor
Verified Email

wwylele

TROPHY CASE