Search results

perf(ldl): replace brute-force four-squares search

area:searchSOS/Search.lean: SDP encoding, CSDP, rounding, LDLSOS/Search.lean: SDP encoding, CSDP, rounding, LDL

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#59 In leanprover/sos;

· kim-em opened on May 13, 2026

feat(search): relaxation hierarchy / automatic depth search

area:searchSOS/Search.lean: SDP encoding, CSDP, rounding, LDLSOS/Search.lean: SDP encoding, CSDP, rounding, LDL

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#58 In leanprover/sos;

· kim-em opened on May 13, 2026

feat(search): support algebraic-extension SOS coefficients

area:certificateSOS/Certificate.lean: schema, checks predicateSOS/Certificate.lean: schema, checks predicate

area:searchSOS/Search.lean: SDP encoding, CSDP, rounding, LDLSOS/Search.lean: SDP encoding, CSDP, rounding, LDL

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#57 In leanprover/sos;

· kim-em opened on May 13, 2026

feat(search): equality cofactor symmetry reduction

area:certificateSOS/Certificate.lean: schema, checks predicateSOS/Certificate.lean: schema, checks predicate

area:searchSOS/Search.lean: SDP encoding, CSDP, rounding, LDLSOS/Search.lean: SDP encoding, CSDP, rounding, LDL

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#56 In leanprover/sos;

· kim-em opened on May 13, 2026

search: Harrison sos.ml:1638 fails to close (Pythagorean-style 4 ineq + 2 eq)

Status: Open.

#52 In leanprover/sos;

· kim-em opened on May 13, 2026

search: Harrison sos.ml:1617 fails to close (two-equality discriminant-style goal)

Status: Open.

#51 In leanprover/sos;

· kim-em opened on May 13, 2026

feat(search): σ-block symmetry reduction for constrained σ-blocks

area:searchSOS/Search.lean: SDP encoding, CSDP, rounding, LDLSOS/Search.lean: SDP encoding, CSDP, rounding, LDL

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#37 In leanprover/sos;

· kim-em opened on May 12, 2026

REAL_SOSFIELD (positive denominators)

area:reifySOS/Reify.lean: goal parsing, reflectionSOS/Reify.lean: goal parsing, reflection

area:tacticSOS/Tactic.lean: top-level dispatch, syntax, optionsSOS/Tactic.lean: top-level dispatch, syntax, options

roadmapTracked feature on the SOS roadmapTracked feature on the SOS roadmap

Status: Open.

#18 In leanprover/sos;

· kim-em opened on May 11, 2026