Extraction of tactics from syntax tree #9

New Issue

aniva · 2023-08-24T23:20:14-07:00

aniva commented

2023-08-24 23:20:14 -07:00

The value stored in a theorem is in the lambda expression form which isn't how the theorems were written. Most theorems were proven in a mixture of tactics and proof terms. The extraction of such tactic sequences is critical to training LLMs.

aniva added this to the 0.2.6 milestone 2023-08-24 23:20:14 -07:00

aniva added the

labels 2023-08-24 23:20:14 -07:00

aniva self-assigned this 2023-08-24 23:20:14 -07:00

aniva removed the

priority

low

label 2023-09-07 20:24:14 -07:00

aniva commented

2023-10-15 19:23:26 -07:00

References:

References: 1. [LeanInk](https://github.com/leanprover/LeanInk/tree/main) 2. [lean-training-data](https://github.com/semorrison/lean-training-data)

aniva modified the milestone from 0.2.6 to 0.3

2023-10-28 16:38:36 -07:00

aniva added reference library/trace

2023-11-06 11:13:11 -08:00

aniva commented

2024-03-18 10:11:35 -07:00

This is temporarily superseded by atomization in Trillium.

aniva removed this from the 0.3 milestone 2024-03-18 10:11:41 -07:00

aniva changed title from ~~Allow the extraction of tactic based proof steps~~ to Extraction of tactics from syntax tree

2024-04-11 17:55:42 -07:00

aniva added

part/Frontend

and removed

part/Environemnt

labels 2024-04-11 17:56:39 -07:00

aniva commented

2024-05-31 20:27:45 -07:00

Solved by #76

aniva closed this issue

2024-05-31 20:27:45 -07:00

Sign in to join this conversation.

No Label

No Milestone

No project

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#9