Commits

Branch selector

 main

User selector

All users

All time

Commit History

Commits on Apr 9, 2026

• Make agent loop action-based: planner chooses what to do next

  Show description for ee8ad3c
  

  sheneman

  and

  claude

  committed
  ee8ad3c

  Copy full SHA for ee8ad3c

• Fix 6 information flow breaks in the agent loop

  Show description for 6f4908e
  

  sheneman

  and

  claude

  committed
  6f4908e

  Copy full SHA for 6f4908e

Commits on Apr 8, 2026

• Add creativity agent for lateral thinking about proof strategies

  Show description for cebe702
  

  sheneman

  and

  claude

  committed
  cebe702

  Copy full SHA for cebe702

• Add trashcan icon to session list for quick delete (no confirmation)

  Show description for d025fdc
  

  sheneman

  and

  claude

  committed
  d025fdc

  Copy full SHA for d025fdc

• Fix delete confirmation message — global lessons are preserved

  Show description for d3fb915
  

  sheneman

  and

  claude

  committed
  d3fb915

  Copy full SHA for d3fb915

• Add delete session button to dashboard GUI

  Show description for 02d1897
  

  sheneman

  and

  claude

  committed
  02d1897

  Copy full SHA for 02d1897

• Add diagnostic analysis — agent reasons about WHY proofs fail

  Show description for dc102c5
  

  sheneman

  and

  claude

  committed
  dc102c5

  Copy full SHA for dc102c5

• Don't auto-add imports from retrieval modules — some aren't built

  Show description for dd59d18
  

  sheneman

  and

  claude

  committed
  dd59d18

  Copy full SHA for dd59d18

• Add by-block collapse to fix the most common indentation bug

  Show description for f52bdc0
  

  sheneman

  and

  claude

  committed
  f52bdc0

  Copy full SHA for f52bdc0

• Add exact? feedback loop and full lemma signatures

  Show description for a2bd0f2
  

  sheneman

  and

  claude

  committed
  a2bd0f2

  Copy full SHA for a2bd0f2

• Tell lean agent to use exact fully-qualified lemma names and add imports

  Show description for cefb6d1
  

  sheneman

  and

  claude

  committed
  cefb6d1

  Copy full SHA for cefb6d1

• Stop auto-extractor from promoting raw error strings as global lessons

  Show description for 34624fe
  

  sheneman

  and

  claude

  committed
  34624fe

  Copy full SHA for 34624fe

• Guide planner web search toward Lean 4 / Mathlib4 only

  Show description for 581019b
  

  sheneman

  and

  claude

  committed
  581019b

  Copy full SHA for 581019b

• Stop web search from polluting lessons and code synthesis

  Show description for ae22bb6
  

  sheneman

  and

  claude

  committed
  ae22bb6

  Copy full SHA for ae22bb6

• Fix the core indentation bug via prompting: single-line have, explicit examples

  Show description for b902d63
  

  sheneman

  and

  claude

  committed
  b902d63

  Copy full SHA for b902d63

• Rename Leanstral → Lean Agent in dashboard UI

  Show description for 3f92337
  

  sheneman

  and

  claude

  committed
  3f92337

  Copy full SHA for 3f92337

• Drop Leanstral, use qwen/qwen3.5-122b as the lean agent

  Show description for 4ca6e86
  

  sheneman

  and

  claude

  committed
  4ca6e86

  Copy full SHA for 4ca6e86

• Use Leanstral's complete file output directly instead of re-wrapping

  Show description for 31e7cab
  

  sheneman

  and

  claude

  committed
  31e7cab

  Copy full SHA for 31e7cab

• Use Leanstral as intended: complete sorry in real Lean files with context

  Show description for e51918c
  

  sheneman

  and

  claude

  committed
  e51918c

  Copy full SHA for e51918c

• Auto-fix hallucinated lemma names using retrieval search

  Show description for 29a31a8
  

  sheneman

  and

  claude

  committed
  29a31a8

  Copy full SHA for 29a31a8

• Fix formatter pop logic: don't pop when content_indent is unknown yet

  Show description for 1cccabb
  

  sheneman

  and

  claude

  committed
  1cccabb

  Copy full SHA for 1cccabb

• Lean-aware formatter: correctly indents sibling have/let/exact statements

  Show description for b8d6a35
  

  sheneman

  and

  claude

  committed
  b8d6a35

  Copy full SHA for b8d6a35

• Fix indentation via prompting: tell Leanstral the Lean 4 indent rules

  Show description for 5c7de58
  

  sheneman

  and

  claude

  committed
  5c7de58

  Copy full SHA for 5c7de58

• Add lean-fmt as final formatting pass for Lean source

  Show description for 6d56294
  

  sheneman

  and

  claude

  committed
  6d56294

  Copy full SHA for 6d56294

• Smarter indentation normalizer: map original indent levels to 2-space depths

  Show description for 26fa2be
  

  sheneman

  and

  claude

  committed
  26fa2be

  Copy full SHA for 26fa2be

• Add tactic indentation normalizer before Lean compilation

  Show description for b1732f6
  

  sheneman

  and

  claude

  committed
  b1732f6

  Copy full SHA for b1732f6

• Fix auto-formalization truncation: collect multi-line theorem statements

  Show description for d25bcac
  

  sheneman

  and

  claude

  committed
  d25bcac

  Copy full SHA for d25bcac

• Fix double-indentation: respect Leanstral's own indentation structure

  Show description for 5d173e4
  

  sheneman

  and

  claude

  committed
  5d173e4

  Copy full SHA for 5d173e4

• Fix Leanstral usage: temperature 1.0, full proof context, no JSON constraint

  Show description for bdf7ab3
  

  sheneman

  and

  claude

  committed
  bdf7ab3

  Copy full SHA for bdf7ab3

• Fix critical indentation bug: indent ALL tactic lines, not just the first

  Show description for 19b0b94
  

  sheneman

  and

  claude

  committed
  19b0b94

  Copy full SHA for 19b0b94

• Use structured JSON output for Leanstral — guaranteed clean tactics

  Show description for f5c468c
  

  sheneman

  and

  claude

  committed
  f5c468c

  Copy full SHA for f5c468c

• Fix duplicate events: deduplicate SSE stream by event ID

  Show description for 62bd80a
  

  sheneman

  and

  claude

  committed
  62bd80a

  Copy full SHA for 62bd80a

• Fierce Leanstral prompts: USE the lemmas, keep it SHORT, no reproof

  Show description for 109e540
  

  sheneman

  and

  claude

  committed
  109e540

  Copy full SHA for 109e540

Commits on Apr 7, 2026

• Aggressive Leanstral output cleaning: extract only valid Lean 4 tactics

  Show description for d472730
  

  sheneman

  and

  claude

  committed
  d472730

  Copy full SHA for d472730

• Fix truncation: increase event display limits, improve code fence stripping

  Show description for 5db309d
  

  sheneman

  and

  claude

  committed
  5db309d

  Copy full SHA for 5db309d