siddhartha-gadgil/LeanAide

Issues

• More efficient embedding lookup

  #45 opened 3 months ago by siddhartha-gadgil
  2

• Multi-shot translation

  #46 opened 3 months ago by siddhartha-gadgil
  1

• Include more information while pretty-printing

  #47 opened 3 months ago by siddhartha-gadgil
  2

• Save translations generated as prompt resources

  #49 opened 3 months ago by siddhartha-gadgil
  0

• Add definitions in roundtrip prompt

  #48 opened 3 months ago by siddhartha-gadgil
  0

• Elaboration check at command level only

  #42 opened 3 months ago by siddhartha-gadgil
  2

• about the prompts_subprocesses.py file

  #43 opened 3 months ago by sushrutjog
  2

• Targeted rewrite: conv_rw?

  #27 opened a year ago by siddhartha-gadgil
  8

• LaTeX converted partially to unicode

  #6 opened a year ago by siddhartha-gadgil
  11

• Aesop cleaner running

  #29 opened a year ago by siddhartha-gadgil
  3

• Speed up search for nearest embeddings

  #31 opened a year ago by siddhartha-gadgil
  1

• Introduce terms and lemmas based on context

  #28 opened a year ago by siddhartha-gadgil
  0

• Prompts for formulas, ellipses, subscripts, idioms, terminology

  #2 opened 2 years ago by siddhartha-gadgil
  11

• Use docstrings from definitions as well as theorems

  #9 opened a year ago by siddhartha-gadgil
  6

• Repeat queries if no outputs

  #30 opened a year ago by siddhartha-gadgil
  1

• Better Equivalence proving

  #3 opened a year ago by siddhartha-gadgil
  6

• Use mathport translations

  #4 opened a year ago by siddhartha-gadgil
  3

• Evaluation data

  #1 opened 2 years ago by siddhartha-gadgil
  3

• Improve keyword-based prompting

  #10 opened 2 years ago by 0art0
  4

• Benchmark and optimize steps of translation

  #8 opened 2 years ago by siddhartha-gadgil
  2

• Case transformations for dot notation

  #7 opened 2 years ago by siddhartha-gadgil
  3

• Using codeActions

  #5 opened 2 years ago by siddhartha-gadgil
  53

• Clean up, abstract configuration

  #19 opened 2 years ago by siddhartha-gadgil
  7

• Lean-chat++

  #12 opened 2 years ago by ayush1801
  1

• Move `yake` to the server

  #15 opened 2 years ago by siddhartha-gadgil
  0

• Rudimentary Proof search step using "first tactic" prompts

  #11 opened 2 years ago by siddhartha-gadgil
  4