Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 9 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Harmonic Functions and the Poisson Integral — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

log|z| is harmonic on the punctured plane

Example

On C∖{0}, the function

u(z)=log⁡∣z∣=12log⁡(x2+y2)

is harmonic.

Facts & Assumptions

Given: The function u(x,y)=12log⁡(x2+y2) on (x,y)≠(0,0).

[L1]

The real logarithm satisfies (log⁡t)′=1/t for t>0 (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

Verification

technique · direct
1.1L1algebra

Differentiating with [L1] gives ux=xx2+y2,uy=yx2+y2.

2.1step 1.1algebra

Differentiating once more gives uxx=y2−x2(x2+y2)2,uyy=x2−y2(x2+y2)2.

3.1step 2.1∎

The sum in step 2.1 is 0, so uxx+uyy=0 on C∖{0}; by Plane harmonic functions, u is harmonic there.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The real parts of z^n are harmonic polynomials

Example

For every integer n≥1, the real part of zn is a harmonic polynomial on C. For instance,

Re⁡(z)=x,Re⁡(z2)=x2−y2,Re⁡(z3)=x3−3xy2.

Verification

technique · direct
1.1L1

The polynomial f(z)=zn is entire by [L1], hence holomorphic on all of C.

2.1step 1.1L2∎

Its real and imaginary parts are polynomials in x and y, so they are of class C∞ and in particular C2; [L2] therefore makes Re⁡(zn) harmonic.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

2xy is a harmonic conjugate of x^2-y^2

Example

The function v(x,y)=2xy is a harmonic conjugate of u(x,y)=x2−y2 on all of C.

Facts & Assumptions

Given: The polynomial f(z)=z2.

[L2]

If a holomorphic function is written u+iv, then its imaginary part is a harmonic conjugate of its real part (The C2 real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair, Harmonic conjugates).

Verification

technique · direct
1.1givenalgebra

Since z2=(x+iy)2=(x2−y2)+2ixy, the real part of z2 is x2−y2 and the imaginary part is 2xy.

2.1step 1.1L1L2∎

The polynomial z2 is entire by [L1], so [L2] makes 2xy a harmonic conjugate of x2−y2.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The Poisson integral of cos(theta) is r cos(theta)

Example

For the boundary datum φ(eiθ)=cos⁡θ, the Poisson integral is

P[φ](reiϕ)=rcos⁡ϕ.

Verification

technique · direct
1.1L2

The function u(reiϕ)=rcos⁡ϕ is the real part of z, so [L2] makes it harmonic on D.

2.1step 1.1L1∎

On the boundary ∣z∣=1, the same formula gives u(eiθ)=cos⁡θ=φ(eiθ). By [L1], the continuous harmonic extension of φ is unique, so P[φ]=u.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-26Open item page →

The Poisson kernel realizes the sharp Harnack bounds on concentric discs

Example

The positive harmonic function

u(z):=P(z,1)=1−∣z∣2∣1−z∣2(∣z∣<1)

satisfies, for every 0≤r<1,

u(rei0)=1+r1−r,u(reiπ)=1−r1+r.

Since u(0)=1, these are exactly the two Harnack bounds on the circle ∣z∣=r.

Facts & Assumptions

Given: A radius 0≤r<1.

[L1]

For z=ρeiϕ, the Poisson kernel at the boundary point 1=ei0 is P(z,1)=1−ρ21−2ρcos⁡ϕ+ρ2 (The Poisson kernel on the unit disc).

[L3]

Positive harmonic functions on a disc satisfy Harnack's inequality (Positive harmonic functions on a disc satisfy Harnack's inequality).

Verification

technique · direct
1.1L1L2algebra

The function H(z):=1+z1−z is holomorphic on ∣z∣<1 by [L2], and its real part is Re⁡H(ρeiϕ)=1−ρ21−2ρcos⁡ϕ+ρ2=P(ρeiϕ,1) by [L1]. Therefore u(z):=P(z,1) is harmonic on the unit disc. Since 1−∣z∣2>0 and ∣1−z∣2>0 for ∣z∣<1, it is positive there as well.

1.2L1algebra

Substituting ϕ=0 and ϕ=π into [L1] gives u(rei0)=1−r2(1−r)2=1+r1−r,u(reiπ)=1−r2(1+r)2=1−r1+r, and u(0)=P(0,1)=1.

2.1step 1.1step 1.2L3∎

Fix R with r<R<1. The function u is harmonic on a neighbourhood of D(0,R)‾, so [L3] gives R−rR+r u(0)≤u(reiϕ)≤R+rR−r u(0). Letting R→1− yields the unit-disc Harnack bounds 1−r1+r≤u(reiϕ)≤1+r1−r. Step 1.2 shows equality at ϕ=π and ϕ=0, respectively. Thus the Poisson kernel realizes both Harnack extremes on the circle ∣z∣=r.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

log|z| has no global harmonic conjugate on C{0}

Statement refuted

Refuted claim: every harmonic function on a domain has a global harmonic conjugate.

The witness is u(z)=log⁡∣z∣ on C∖{0}. It is harmonic there, but it has no global harmonic conjugate.

Facts & Assumptions

Given: The harmonic function u(z)=log⁡∣z∣ on C∖{0}.

[L1]

The function log⁡∣z∣ is harmonic on the punctured plane (log|z| is harmonic on the punctured plane).

[L2]

There is no continuous logarithm on all of C∖{0} (There is no continuous logarithm on all of C∖{0}).

[L3]

The complex exponential is entire, satisfies exp⁡(α−β)=exp⁡(α)/exp⁡(β), and compositions and quotients of holomorphic functions are holomorphic wherever the denominator is nonzero (The complex exponential is entire and its complex derivative is itself, exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential, The chain rule for complex derivatives, Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L4]

A nonconstant holomorphic function on a complex domain is an open map (Open mapping theorem for holomorphic functions).

Counterexample

technique · direct
1.1assume-contra

Suppose v were a harmonic conjugate of log⁡∣z∣ on C∖{0}. Then F(z):=log⁡∣z∣+iv(z) would be holomorphic there, and its exponential would satisfy exp⁡(F(z))=∣z∣(cos⁡v(z)+isin⁡v(z)).

2.1step 1.1L3L4algebra

The function G(z):=exp⁡(F(z))/z is holomorphic on C∖{0} by [L3], and ∣G(z)∣=∣exp⁡(F(z))∣/∣z∣=eRe⁡F(z)/∣z∣=1 by step 1.1. If G were nonconstant, [L4] would make its image open in C, impossible because G(C∖{0})⊆{ ∣w∣=1 }. Hence G is constant on C∖{0}.

3.1step 2.1L2L3

Since G is constant, for every z≠0 one has exp⁡(F(z)−F(1))=exp⁡(F(z))exp⁡(F(1))=z G(z)G(1)=z. Thus L(z):=F(z)−F(1) is a continuous logarithm on C∖{0}, contradicting [L2].

4.1step 3.1L1discharge-contradiction∎

Therefore log⁡∣z∣ has no global harmonic conjugate on C∖{0}.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

A harmonic function can vanish on a line without being zero everywhere

Statement refuted

Refuted claim: if a harmonic function vanishes on a line segment, then it vanishes identically on its domain.

The witness is

u(x,y)=x.

It is harmonic on C, vanishes on the whole y-axis, and is not the zero function.

Facts & Assumptions

Given: The function u(x,y)=x.

Counterexample

technique · direct
1.1algebra

One has uxx=0 and uyy=0, so uxx+uyy=0 and u is harmonic on C by Plane harmonic functions.

2.1step 1.1algebra∎

On the line x=0, the function u vanishes identically, but u(1,0)=1≠0. So vanishing on a line does not force vanishing everywhere.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The product of two harmonic functions need not be harmonic

Statement refuted

Refuted claim: the product of two harmonic functions is always harmonic.

The witness is u(x,y)=x and v(x,y)=x. Each factor is harmonic, but their product is x2, whose Laplacian is 2.

Facts & Assumptions

Given: The functions u(x,y)=x and v(x,y)=x.

Counterexample

technique · direct
1.1algebra

As in the previous example, u and v are harmonic because both have vanishing second partial derivatives.

2.1step 1.1algebra∎

Their product is uv=x2, and (x2)xx+(x2)yy=2+0=2≠0. So uv is not harmonic.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Re(1/z) is harmonic on a punctured disc and does not extend harmonically across 0

Statement refuted

Refuted claim: every harmonic function on a punctured disc extends harmonically across the puncture.

The witness is

u(z)=Re⁡(1/z).

It is harmonic on 0<∣z∣<1, but it is unbounded near 0 and therefore does not extend harmonically there.

Facts & Assumptions

Given: The function f(z)=1/z on 0<∣z∣<1 and its real part u(z)=Re⁡(f(z)).

[L3]

A bounded harmonic function near an isolated puncture does extend harmonically (A bounded harmonic function near an isolated puncture extends harmonically).

Counterexample

technique · direct
1.1L1L2

By [L1], the function 1/z is holomorphic on 0<∣z∣<1, so [L2] makes u(z)=Re⁡(1/z) harmonic there.

1.2L3algebra

On the positive real axis, u(t)=1/t→+∞ as t↓0, so u is unbounded near 0. If u had a harmonic extension across 0, it would be bounded on some small closed disc around 0, contradicting [L3].

2.1step 1.1step 1.2∎

Therefore u is harmonic on the punctured disc but does not extend harmonically across the puncture.

Sources