{"root":"root","nodes":[{"id":"root","parent":null,"title":"聚合与收口","kind":"aggregate","specid":null,"params":{},"deps":[],"weight":1200},{"id":"stmt","parent":"root","title":"命题陈述：非零项数与平方项数的界（锁定到具体文献定理）","kind":"formalize","specid":null,"params":{"target":"Jsp393/Statement.lean"},"deps":[],"weight":3200},{"id":"core","parent":"root","title":"关键引理形式化（真证明、无 sorry、无自定义公理）","kind":"formalize","specid":null,"params":{"target":"Jsp393/Core.lean"},"deps":[],"weight":5600}]}