The primary goal of Project LANA is to digitize definitions and results from anabelian geometry using the Lean4 interactive proof assistant. LANA is an acronym, standing for “Lean for ANAbelian geometry”. Additional details will be added soon.