All Bounties
Open Bounties
- -- Antihydra Halts? --... - Bounty: 0.006 ETH
- -- primes are infinite import... - Bounty: 0.05 ETH
- -- subset relation is transitive for... - Bounty: 0.03 ETH
- import Mathlib.Data.Nat.GCD.Basic -- Prove... - Bounty: 0.02 ETH
- -- double negation theorem double_negation {P... - Bounty: 0.001 ETH
- -- commutativity of addition theorem add_comm... - Bounty: 0.05 ETH
- -- Miller Rabin Fixed Repetition... - Bounty: 0.0017 ETH
- import Mathlib theorem pi_transcendental (p :... - Bounty: 0.0017 ETH
- import Mathlib theorem pi_transcendental (p :... - Bounty: 0.0001 ETH
Closed Bounties
- theorem debug (n : Nat) : n + 4 = n + 4 := sorry - Bounty: 0.0005 ETH
- -- Both the bounty and the submission should... - Bounty: 0.0005 ETH
- theorem self_eq_self (n : Nat) : n + 1 = n +... - Bounty: 0.0003 ETH
- -- Prove that reversing a list does not change... - Bounty: 0.02 ETH
- -- Composition of two injective functions is... - Bounty: 0.04 ETH
- -- De Morgan's law theorem demorgan_not_or (P... - Bounty: 0.03 ETH
- import Mathlib theorem four_squares (n : Nat)... - Bounty: 0.0003 ETH
- -- Prove that P ∧ (Q ∨ R) implies (P ∧ Q) ∨ (P... - Bounty: 0.002 ETH
- -- Prove that from P ∨ Q and ¬P, we can... - Bounty: 0.002 ETH
- theorem reverse_reverse {α : Type} (l : List... - Bounty: 0.0011 ETH
- theorem imp_trans (P Q R : Prop) (h1 : P -> Q)... - Bounty: 0.0014 ETH
- theorem zero_add (n : Nat) : 0 + n = n := sorry - Bounty: 0.0008 ETH
- import Mathlib theorem self_eq_self (n : Nat)... - Bounty: 0.0013 ETH
- theorem self_eq_self (n : Nat) : n = n := sorry - Bounty: 0.0023 ETH