mirek/Vibe-ITP
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Interactive theorem prover. Human-written kernel & axioms, AI-written proof language & proofs (with some human help). Based on 2nd-order logic & set-theory.
46 commits 1 branch 0 tags 228 MiB
  • C++ 96.3%
  • C 2.5%
  • Shell 0.9%
  • Emacs Lisp 0.2%
  • Makefile 0.1%
Find a file
Exact
Codex e671155fea Update JIT imports and arithmetic setup
2026-09-24 08:50:50 +02:00
lean Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
affine-order-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
affine.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
AGENTS.md merge temporary challenges into the proof files 2026-05-27 22:52:44 +02:00
analysis-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
analysis-fta.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
analysis.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
analysis.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
application.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
arithmetics-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
arithmetics-features-showcase.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
arithmetics.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
automation-feature-highlights-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
aux-def-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
basic-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
basic.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
binary_export.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
binary_export.h Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
binary_spec.md starting with meta-reasoning 2026-05-30 23:16:17 +02:00
binder-rewrite-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
binder-simplifier-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
bytecode.cpp starting with meta-reasoning 2026-05-30 23:16:17 +02:00
check.c Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
check.h starting with meta-reasoning 2026-05-30 23:16:17 +02:00
check_test.c starting with meta-reasoning 2026-05-30 23:16:17 +02:00
code-reasoning.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
complex-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
complex-metric.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
complex-root.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
complex.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
complex.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
constructors-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
constructors.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
continuity.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
deriv-basic.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
deriv-mean.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
emulator.cpp Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
equality.cpp meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
extensionality-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
extensionality.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
fact-universal-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
facts.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
higher-order-apply-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
inception_jit.c further development, binary checker format, reasoning about tuples 2026-05-20 14:17:28 +02:00
induction-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
induction.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
jit-challenge.lg Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
jit_demo.c Arithmetics x86_64 specification 2026-05-24 03:19:01 +02:00
jit_demo.pf Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
lg-mode.el progress on code verification 2026-05-27 04:00:41 +02:00
limits.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
lit-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
lit.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
logic.c meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
logic.h starting with meta-reasoning 2026-05-30 23:16:17 +02:00
logic.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
Makefile Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta-binder-test.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta-binder-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta-lifting.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta-lit.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta-rules.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta.cpp meta theory mostly done 2026-06-04 23:02:44 +02:00
meta.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
meta.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
natbits-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
natbits.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
parser.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
polynomial-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
polynomial.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
polynomial.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
positivity-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prime-challenge.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prime-loop-code.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prime-loop.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prime-main.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prime.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
properties.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
proposals.md meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
prover-features-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prover.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
prover.md Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
README.md meta theory mostly done 2026-06-04 23:02:44 +02:00
realext-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
realext.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
reals-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
reals.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
reals.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
records.cpp meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
records.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
rectangle-extrema.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
relational-calc-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
relations.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
riemann-integral-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
riemann-integral.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
riemann-integral.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
ring-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
ring.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
set-theory-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
set-theory.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
simplifier-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
simplifier.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
simplifier_binders.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
spec-x86_64.lg Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
spec2.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
summation-test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
summation.cpp Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
test.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
todo Update JIT imports and arithmetic setup 2026-09-24 08:50:50 +02:00
tuple-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
tuple.cpp meta reasoning progress 2026-05-31 13:57:51 +02:00
tuple.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-arith-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-arith.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-arith.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-op.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-op.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-real-op-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-real-op.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-real-op.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-topo-challenges.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-topo.lg Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ-topo.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00
univ.pf Add universal mathematics and Lean checker 2026-09-24 08:49:00 +02:00

README.md

Vibe ITP

Try out:

make
# in any order
./parser logic.lg
./prover logic.lg set-theory-challenges.lg arithmetics-challenges.lg lit-challenges.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf
# Code verification stack
./prover logic.lg spec-x86_64.lg prime-challenge.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf natbits.pf tuple.pf univ.pf records.pf code-reasoning.pf prime.pf prime-loop.pf prime-loop-code.pf prime-main.pf
# Meta-theory stack
./prover logic.lg meta.lg meta-binder-test.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf natbits.pf tuple.pf univ.pf records.pf meta.pf meta-lifting.pf meta-rules.pf meta-binder-test.pf meta-lit.pf

File structure

  • logic.lg: definitions & axioms (human written)
  • logic.c: the logical kernel (human written)
  • *.pf: proof files
  • *-challenges.lg: target problems
  • *.cpp: the parsing & proving features
  • emulator.cpp, *jit*: experiments with binary code, not related to the rest