Search results

smt_show [*] fails on polymorphic Monoid goals (incorrect number of universe levels Monoid)

Status: Open.

#230 In ufmg-smite/lean-smt;

· alexhkurz opened on Jun 9, 2026

Version without Mathlib?

Status: Open.

#228 In ufmg-smite/lean-smt;

· spaceunifyfifty opened on Apr 30, 2026

smt fails with failed to create binder due to failure when reverting variable dependencies

Status: Open.

#224 In ufmg-smite/lean-smt;

· zqy1018 opened on Mar 27, 2026

cannot translate 0

Status: Open.

#223 In ufmg-smite/lean-smt;

· sicheng-tan opened on Mar 19, 2026

How to appropriately use Lean-smt for Dalek-lean verification

Status: Open.

#222 In ufmg-smite/lean-smt;

· Zhang-Liao opened on Mar 16, 2026

4.28 ?

Status: Open.

#218 In ufmg-smite/lean-smt;

· spitters opened on Feb 23, 2026

Model values should be of the pre-embedding type

Status: Open.

#208 In ufmg-smite/lean-smt;

· dranov opened on Dec 23, 2025

Closing goals that involve Nat

Status: Open.

#204 In ufmg-smite/lean-smt;

· F47-503 opened on Oct 9, 2025

Proof reconstruction fails for Bool

Status: Open.

#192 In ufmg-smite/lean-smt;

· dranov opened on Aug 19, 2025

error: C++ to Lean enum translation failed with exit code 1:

Status: Open.

#188 In ufmg-smite/lean-smt;

· nnarek opened on Jul 31, 2025

Request for Sledgehammer evaluation dataset access

Status: Open.

#186 In ufmg-smite/lean-smt;

· kapeYuan opened on Jun 22, 2025

Cannot translate nat_lit due to Nat.add

Status: Open.

#185 In ufmg-smite/lean-smt;

· dranov opened on Jun 19, 2025