import Mathlib

def hello := "world"