Proof Assistants Beta
tinlyx's user avatar
tinlyx's user avatar
tinlyx's user avatar
tinlyx
  • Member for 1 year, 3 months
  • Last seen this week
Profile Activity

15 Questions

Score Activity Newest Views
15 votes
3 answers
255 views

Proof assistants for forward reasoning?

12 votes
2 answers
252 views

Does Lean have a standard ASCII representation?

12 votes
3 answers
638 views

Can the language of proof assistants be used for general purpose programming?

8 votes
1 answer
40 views

Are `subclass` and `instance` commands equivalent in defining subclass relation between typeclasses in Isabelle?

8 votes
2 answers
78 views

Is there a way to convert free variables to (meta) universally quantified variables in Isabelle?

8 votes
2 answers
160 views

How to prove Gauss summation of integers with proof assistants using forward reasoning?

8 votes
2 answers
198 views

What is the computational complexity of theorem proving?

7 votes
1 answer
121 views

Is there a way to use sledgehammer in Isar proofs?

6 votes
1 answer
233 views

How to install Lean-4 stable only?

5 votes
1 answer
56 views

How to rename a type class operator in a subclass in Isabelle/HOL?

5 votes
1 answer
142 views

Is ACL2 first-order-logic and is this a limitation for proving math?

4 votes
2 answers
354 views

How to run the main function in lean 4?

4 votes
2 answers
292 views

Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

3 votes
0 answers
28 views

How to prove that a non-negative nat is positive in J-Bob?

3 votes
1 answer
122 views

untyped lambda expressions may not have normal forms; are they used (or OK to use) in proof assistants?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.