Update app.py

app.py

@@ -5,15 +5,26 @@ from transformers import AutoTokenizer, AutoModelForCausalLM, GenerationConfig
 import torch
 import json
 
-LEAN4_DEFAULT_HEADER = "import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n"
+LEAN4_DEFAULT_HEADER = (
+    "import Mathlib\n"
+    "import Aesop\n\n"
+    "set_option maxHeartbeats 0\n\n"
+    "open BigOperators Real Nat Topology Rat"
+)
 
 title = """# 🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉
 You can build with this endpoint using🔮Goedel-Prover-SFT📉 available here : [Goedel-LM/Goedel-Prover-SFT](https://huggingface.co/Goedel-LM/Goedel-Prover-SFT)."""
 
 def format_prompt(formal_statement, informal_prefix=""):
     """Format the input according to the Lean4 structure"""
-    return f"Complete the following Lean 4 code with explanatory comments preceding each line of code:\n\n```lean4\n{LEAN4_DEFAULT_HEADER}{informal_prefix}{formal_statement}"
-
+    return (
+        f"Complete the following Lean 4 code with explanatory comments preceding each line of code:\n\n"
+        f"```lean4\n"
+        f"{LEAN4_DEFAULT_HEADER}\n"
+        f"{informal_prefix}\n"
+        f"{formal_statement}"
+    )
+    
 def extract_code(response):
     """Extract code between lean4 code blocks and the model's output"""
     try: