Search results

[IK]: Prove LSeries_totient_eq

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1291 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 22, 2026

[IK]: Prove liouville_eq_moebius_on_squarefree

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1290 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 22, 2026

[IK]: Prove IsCompletelyMultiplicative.isMultiplicative

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1289 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 22, 2026

[IK]: Prove IsCompletelyMultiplicative.mul

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1288 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 22, 2026

[IK]: Prove LSeries_liouville_eq

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1286 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 22, 2026

[IK]: prove moebius_sq_eq

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1276 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 15, 2026

[IK]: Prove zeta_alt

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1275 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 15, 2026

[IK]: Prove zeta_pow_two

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1274 In AlexKontorovich/PrimeNumberTheoremAnd;

· AlexKontorovich opened on Apr 15, 2026

[BKLNW]: Explicit lower bound on theta using Table 12 (Corollary 9.1)

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1264 In AlexKontorovich/PrimeNumberTheoremAnd;

· teorth opened on Apr 5, 2026

[BKLNW]: Verify Table 12

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1263 In AlexKontorovich/PrimeNumberTheoremAnd;

· teorth opened on Apr 5, 2026

[BKLNW]: Lower bound on theta for small x (Corollary 9.1)

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1262 In AlexKontorovich/PrimeNumberTheoremAnd;

· teorth opened on Apr 5, 2026

[BKLNW]: Importing Table 1 from Buthe

taskThe issue is a formalisation task.The issue is a formalisation task.

Status: Open.

#1261 In AlexKontorovich/PrimeNumberTheoremAnd;

· teorth opened on Apr 5, 2026