# Overview The 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, [[Formalising Mathematics - Metha]]: ![[File header boilerplate-1.png]] Note that the LeanNotes wiki page that annotates this file has the same name as the file being annotated, [[Sheet1.lean]] ## 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: Den Ducoff, Gemini 3.5 # Read Me First A list of the tactics used in this file are available in LeanNotes wiki page: <LeanNotes wiki page url> -/ ``` --- Author: [[dducoff]] Posted Date: 2026-06-26