felipeperet

felipeperet/Lean-blaster

SMT-based reasoning core for Lean4

0 stars 0 forks 0 watchers Lean Apache License 2.0

2 Open Issues Need Help Last updated: Jul 28, 2026

Open Issues Need Help

View All on GitHub

[Int] Emit proof steps for the Int.mul rules (0*n, 1*n) 6 days ago

good first issue

felipeperet/Lean-blaster

0

SMT-based reasoning core for Lean4

Lean

[Int] Emit proof step for the 0 + n ⟹ n rule (Int.add) 6 days ago

good first issue

felipeperet/Lean-blaster

0

SMT-based reasoning core for Lean4

Lean