Email now includes proof.lean and research_log.md attachments

- proof.lean: the Lean 4 code file
- research_log.md: full research log with all tool calls, search results,
Lean code attempts, and error messages
- Agent captures detailed log of every tool call and result

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

agent.py

@@ -170,13 +170,20 @@ async def run_agent(question: str):
     )
     cost_tracker = CostTracker()
     status_log: list[str] = []
+    full_log: list[str] = []  # Detailed log with tool contents
 
     def add_status(msg: str):
         status_log.append(msg)
 
+    def log_detail(msg: str):
+        full_log.append(msg)
+
     def render_status():
         return "\n".join(f"- {s}" for s in status_log)
 
+    def get_full_log():
+        return "\n\n".join(full_log)
+
     messages: list[dict] = [
         {"role": "system", "content": SYSTEM_PROMPT},
         {"role": "user", "content": question},
@@ -228,6 +235,8 @@ async def run_agent(question: str):
         messages.append(msg_dict)
 
         if not assistant_msg.tool_calls:
+            if assistant_msg.content:
+                log_detail(f"## Agent thinking\n{assistant_msg.content}")
             add_status("Thinking...")
             yield render_status(), None
             continue
@@ -239,15 +248,20 @@ async def run_agent(question: str):
             except json.JSONDecodeError:
                 fn_args = {}
 
+            log_detail(f"## Tool call: `{fn_name}`\n**Args:** ```json\n{json.dumps(fn_args, indent=2)[:2000]}\n```")
+
             result = await _handle_tool_call(
                 fn_name, fn_args, add_status, render_status,
-                # Pass the yield-like callback for streaming status updates
             )
 
+            log_detail(f"**Result:** ```\n{result[:5000]}\n```")
+
             # final_answer terminates the loop
             if fn_name == "final_answer":
                 add_status("Research complete!")
                 yield render_status(), fn_args
+                # Attach full_log to result for email
+                fn_args["_full_log"] = get_full_log()
                 return
 
             yield render_status(), None

app.py

@@ -42,10 +42,12 @@ async def respond(message, history, email):
             answer = final_result.get("answer", "") if final_result else ""
             lean_code = final_result.get("lean_code", "") if final_result else ""
             verified = final_result.get("verified", False) if final_result else False
+            full_log = final_result.get("_full_log", "") if final_result else ""
             sent = send_result_email(
                 to_email=email.strip(),
                 question=message,
                 status_log=status_text,
+                full_log=full_log,
                 answer=answer,
                 lean_code=lean_code,
                 verified=verified,

email_sender.py

@@ -4,6 +4,8 @@ import os
 import smtplib
 from email.mime.text import MIMEText
 from email.mime.multipart import MIMEMultipart
+from email.mime.base import MIMEBase
+from email import encoders
 
 SMTP_HOST = os.getenv("SMTP_HOST", "smtp.gmail.com")
 SMTP_PORT = int(os.getenv("SMTP_PORT", "587"))
@@ -15,11 +17,12 @@ def send_result_email(
     to_email: str,
     question: str,
     status_log: str,
+    full_log: str,
     answer: str,
     lean_code: str,
     verified: bool,
 ) -> bool:
-    """Send research results via email. Returns True on success."""
+    """Send research results via email with attached files. Returns True on success."""
     if not SMTP_EMAIL or not SMTP_PASSWORD:
         print("SMTP not configured, skipping email")
         return False
@@ -27,7 +30,12 @@ def send_result_email(
     badge = "VERIFIED" if verified else "UNVERIFIED (best effort)"
     subject = f"VeriDeepResearch: {question[:60]}{'...' if len(question) > 60 else ''}"
 
-    # Build HTML email
+    msg = MIMEMultipart("mixed")
+    msg["Subject"] = subject
+    msg["From"] = f"VeriDeepResearch <{SMTP_EMAIL}>"
+    msg["To"] = to_email
+
+    # HTML body (concise summary)
     html = f"""\
 <html>
 <body style="font-family: -apple-system, sans-serif; max-width: 800px; margin: 0 auto; padding: 20px;">
@@ -49,7 +57,7 @@ def send_result_email(
 </pre>
 
 <details>
-<summary><strong>Research Log</strong></summary>
+<summary><strong>Status Log</strong></summary>
 <pre style="background: #f0f0f0; padding: 12px; border-radius: 8px; font-size: 12px; white-space: pre-wrap;">
 {_escape(status_log)}
 </pre>
@@ -57,37 +65,42 @@ def send_result_email(
 
 <hr>
 <p style="color: #666; font-size: 12px;">
+Full research log and Lean code attached as files.<br>
 Generated by <a href="https://vilin97-verideepresearch.hf.space">VeriDeepResearch</a>.
 All Lean code checked with Axle (Lean 4.28.0 + Mathlib).
 </p>
 </body>
 </html>
 """
-
-    # Plain text fallback
-    text = f"""\
-VeriDeepResearch Results
-========================
-
-Question: {question}
-Status: {badge}
-
-Answer:
-{answer}
-
-Lean 4 Code:
-{lean_code}
-
-Research Log:
-{status_log}
-"""
-
-    msg = MIMEMultipart("alternative")
-    msg["Subject"] = subject
-    msg["From"] = f"VeriDeepResearch <{SMTP_EMAIL}>"
-    msg["To"] = to_email
-    msg.attach(MIMEText(text, "plain"))
-    msg.attach(MIMEText(html, "html"))
+    body = MIMEMultipart("alternative")
+    body.attach(MIMEText(f"Question: {question}\nStatus: {badge}\n\nAnswer:\n{answer}\n\nSee attached files for Lean code and full research log.", "plain"))
+    body.attach(MIMEText(html, "html"))
+    msg.attach(body)
+
+    # Attachment 1: Lean code (.lean file)
+    if lean_code.strip():
+        lean_attachment = MIMEBase("application", "octet-stream")
+        lean_attachment.set_payload(lean_code.encode("utf-8"))
+        encoders.encode_base64(lean_attachment)
+        lean_attachment.add_header(
+            "Content-Disposition",
+            "attachment",
+            filename="proof.lean",
+        )
+        msg.attach(lean_attachment)
+
+    # Attachment 2: Full research log (.md file)
+    if full_log.strip():
+        log_attachment = MIMEBase("application", "octet-stream")
+        log_content = f"# VeriDeepResearch Full Log\n\n**Question:** {question}\n**Status:** {badge}\n\n---\n\n{full_log}"
+        log_attachment.set_payload(log_content.encode("utf-8"))
+        encoders.encode_base64(log_attachment)
+        log_attachment.add_header(
+            "Content-Disposition",
+            "attachment",
+            filename="research_log.md",
+        )
+        msg.attach(log_attachment)
 
     try:
         with smtplib.SMTP(SMTP_HOST, SMTP_PORT) as server: