Open Research Index

BochaoKong/classical-complex-wpt

BochaoKong

Palomar Registrypalomar/PALOMAR-2026-08-29-000010Aug 29, 2026math.CVscore 0

A Mathlib-only Lean 4 formalization of the classical complex-analytic Weierstrass preparation theorem at the origin. For every number of base variables and every preparation degree, including the zero-dimensional and degree-zero cases, it constructs the distinguished monic polynomial and nonvanishing analytic unit and proves uniqueness of all factors as germs.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-29-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'