# Overview All LeanNote files include a customized version of the header template. Here is a snapshot of the uncustomized header template: ![[File header template-1.png]] Here is the source code for the uncustomized header template: ```Lean /-! # URL: This url links to annotations, copyright, authors, and a README section. [URL goes here] # Summary: This docstring explains the purpose of the code in this file. It must be placed immediately after the imports. -/ ``` Here is an example of a customized version of the header template for the` apply-1.lean `file: #TODO Code that requires acknowledgement of prior copyright notices have a header that includes two sections for the: - copyright and author credits - a Read Me First section that provides a link to the LeanNotes wiki note that annotates the .lean file. The file header boilerplate code has three sections that are specific to each *.lean* file: - **Copyright notice** : If the *.lean* file is a modification of a previously copyrighted work, then the previous copyright notice needs to be retained in full. Otherwise the [[LeanNotes copyright license]] can be used, which designates the software as a free and unencumbered piece of work that is released into the public domain. - **List of authors, including AI** : This comma separated list includes all authors that have made a significant contribution to this *.lean* file, including the AI tutors. - **Read Me First** : This section provides a link to the LeanNotes wiki page that annotates the *.lean* file: # Example headers ## Derived work Here is a snapshot of a header boilerplate from a file, *Sheet-1.lean,* that is derived from the eBook, [[Courses and eBooks/Formalising Mathematics - Metha/Links]]: ![[Appendix/Media/Images/Miscellaneous images/File header boilerplate-1.png]] Note that the LeanNotes wiki page that annotates this file has the same name as the file being annotated, [[Courses and eBooks/Formalising Mathematics - Metha/Table of Contents]] ## Original work Here is an example of a header boilerplate with no previous copyright and only two authors: ```lean /- # Copyright and author credits Copyright (c) 2026, Den Ducoff. No rights reserved. Please refer to https://unlicense.org Authors: Gemini 3.5, Den Ducoff # Read Me First A list of the tactics used in this file are available in LeanNotes wiki page: <LeanNotes wiki page url> -/ ``` --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-11