Sagicc/nanoGentzen

nanoGentzen Synthetic Deduction Dataset (200k Transitions) The nanoGentzen Dataset is a formal synthetic dataset designed to train Policy-Value Transformers for automated theorem proving in Intuitionistic Logic (LI) and Classical Logic (LK via Glivenko's Theorem) using Gentzen Sequent Calculus. Each record represents a single state-action derivation transition along an AND-OR proof search tree, providing multi-task supervision for inference rule selection, antecedent premise… See the full description on the dataset page: https://huggingface.co/datasets/Sagicc/nanoGentzen.