FormalConjecturesTest/Util/Attributes/Basic.lean

GitHub source file

14 declarations, 5 contain sorry, 0 declared as axioms

Imports (4)
  1. theorem test sorry line 30 source

    depends on sorry (Lean reported 5 error(s) in this file) what this means

    Statement uses: Eq, Nat, HAdd.hAdd, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  2. theorem FLT sorry line 35 source

    depends on sorry (Lean reported 5 error(s) in this file) what this means

    Statement uses: FermatLastTheorem

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. theorem an_open_problem sorry line 41 source

    depends on sorry (Lean reported 5 error(s) in this file) what this means

    Statement uses: Transcendental, Real, HAdd.hAdd, Real.pi, Real.exp, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  4. theorem a_formally_solved_problem line 46 source
  5. theorem a_graduate_problem_with_formal_proof line 52 source
  6. theorem a_test_with_formal_proof line 57 source
  7. theorem conditional_formal_proof_hypothesis sorry line 61 source

    depends on sorry (Lean reported 5 error(s) in this file) what this means

    Statement uses: Eq, Nat, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  8. theorem another_conditional_formal_proof_hypothesis sorry line 65 source

    depends on sorry (Lean reported 5 error(s) in this file) what this means

    Statement uses: Eq, Nat, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  9. theorem a_conditionally_formally_solved_problem line 72 source
  10. theorem a_conditionally_formally_solved_problem_with_two_hypotheses line 79 source
  11. theorem conditional_formal_proof_without_assuming line 103 source
  12. theorem assuming_without_conditional_formal_proof line 114 source
  13. theorem a_lean4_proof_with_empty_link line 125 source
  14. theorem a_formal_proof_with_malformed_link line 133 source