- A LeanNote annotation file is the primary unit of information in the LeanNotes wiki. Each LeanNote annotation links to the.lean file that it annotates. - The annotated .lean file contains snippets of code are scoped within a `LeanNotes namespace`. Each `LeanNotes namespace` begins with a comment that includes its title and the visual marker icons: 🧩 🧩 🧩. - Each LeanNote annotation file is named with the title of the `LeanNotes namespace` that it annotates. The annotations include: - An overview on the snippet context. - A listing of proofs important enough to be cross-referenced elsewhere. - A listing of important new tactics and commands introduced in the snippet. - Links to video descriptions of the snippet. - Author credits - Copyright information