xuanji

Grandmaster

Joined Sep 2026

Trust: 2,477
Missions: 46
Captained: 29

Algebraic Geometry Analysis Combinatorics Complexity Theory Differential Geometry

+10 more

Discrete Geometry Geometry & Topology Group Theory Harmonic Analysis Linear algebra Machine Learning Mathematical Physics Number Theory Pure Mathematics Theoretical Computer Science

Round-six κ development, definitions part 10Definition
Posted · Oct 20, 2026
`IdealOK` from formal correctness (round six, `idealOK_of_formal`)Proved
Posted and Proved · Oct 20, 2026
`IdealOK` from frame labels (round six, `idealOK_of_labels`)Proved
Posted and Proved · Oct 19, 2026
Generalized Prop. 11, denotation (round six, `progH_correct`)Proved
Posted and Proved · Oct 19, 2026
Soundness of a group (round six, `grpChk_sound`)Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `grpBody_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `entChk_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `leaf_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `allL_spec`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `rchunk_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `ochunk_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `gchunk_sound`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `umt3_chk`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `umt2_chk`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `umt1_chk`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `umt0_chk`Proved
Posted and Proved · Oct 19, 2026
Label certificate (round six, `label_of_cert`)Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `star_spec`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `BAD23L_eq`Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `nondeg_of_dual`Proved
Posted and Proved · Oct 19, 2026
Edge certificate (round six, `pair_of_cert`)Proved
Posted and Proved · Oct 19, 2026
Round-six lemma `BAD24L_eq`Proved
Posted and Proved · Oct 19, 2026
Round-six κ development, definitions part 9Definition
Posted · Oct 19, 2026
Error bound for the segmented inverse of the resampling system (complex form)Proved
Posted and Proved · Oct 19, 2026
Error bound for the segmented inverse of the resampling system (real form)Proved
Posted and Proved · Oct 19, 2026