# Understand mathematics. Follow the derivation.

A mathematical knowledge system for Chinese and English readers and AI: from concepts and assumptions to examples, step-by-step derivations and traceable evidence.

[Explore questions →](/en/explore/)[Choose a learning path](/en/paths/)

Bilingual question derivations36,000

Knowledge objects302

Concept guides299

Learning paths59



## Choose your starting point



## [Read a complete book](/en/books/)

Read numbers, algebra, geometry, sets, logic and proof, or download the PDFs. Traditional Chinese text.





## [Understand a concept](/en/knowledge/)

Read definitions, assumptions, relationships and exact formulas.





## [Follow a derivation](/en/derivations/)

299 concept guides, distinct from individual question derivations.





## [Practice a topic](/en/practice/)

360 batches with links to bilingual question derivations.





## [Inspect the evidence](/en/formal/)

Inspect Lean sources, exact machine claims and verification limits.









## Understanding verification states



## Question derivations

36,000 have second-context AI mathematical and bilingual semantic review; 0 remain display/symbol-checked candidates.





## Formal evidence

5 Lean evidence objects are linked to 4 knowledge objects; 298 objects have no linked formal evidence.

[Read exact claims and Lean sources](/en/formal/)



## Source and review are separate

Source questions retain candidate and English retains ai_candidate. Second-context AI review is neither human review nor a whole-bank Lean proof. Finite checks support only their stated scope.









## The map is an entry point

Core80 is the stable foundation; the complete current atlas has 302 nodes. Knowledge objects, concept guides, questions and formal evidence are distinct, linked layers.

[Explore the mathematical atlas →](/en/atlas/)