Day 5 Of Learning Lean

Day 5 of learning Lean

why is proving ¬(p ↔ ¬p) so hard

Of course with Truth tables and classical logic, this is near trivial to solve. In fact here's the proof

example : ¬(p ↔ ¬p) := Not.intro λ(Iff.intro pnp npp) => have hnp : ¬p := (imp_iff_not_or.mp pnp).elim id id have hp : p := npp hnp hnp.elim hp

Could be a lot shorter, especially at proving the (¬p ∨ ¬p) part. But you get the gist.

Unfortunately this line exists

imp_iff_not_or is apparently only in classical logic, because it relies on the law of excluded middle which is (p ∨ ¬p) which intuitionistic logic does not have as ¬p is defined as (p -> False).

right now I'm looking into modal logic for solutions and it seems promising, having translations from Intuitional to KT4 modal logic, though I still don't know how I could translate it to a lean solution. It's also very likely there is a simpler solution that I am not seeing.

Either way, it's pretty fun despite my frustrations.

So far still stuck at page 3 of theorem proving in lean 4, though I only have 1 problem to solve.

Anyone else learn languages designed to be proof assistants? Or atleast designed with theorem proving as a usecase. Whilst barely knowing any pure Math?

When I first started learning Idris2, I had no idea how to even structure a proof. Needless to say I was quite lost, even if I was experienced in Haskell at that point.

Even now when I'm learning Lean, when I started which was about 5 days ago, I only knew how to prove with truth tables. It wasn't until yesterday when I found about the logics other than Classical.

So basically all I know about pure math is just me brute-forcing my way into learning languages like Idris as well as the occasional Haskell article or codewars kata ethat deep dives into a concept.

It wasn't until recently when I decided to finally sit down and learn Pure Math starting from basic Discrete Math. It's fun because I keep recognizing the concepts that's become commonplace in the languages I use. I learned about Connection intros and eliminations before knowing the difference between classical and intuitionistic logic.

What I'm saying is I love Curry-Howard correspondence

Nothing hurts more than seeing someone struggle through and be forced to learn something you studied for fun.

is it normal that I'm 18 and I still have absolutely no concept of romantic/sexual attraction or relationships

I ... think I'm bisexual? maybe? but it would be really nice if I could find at least one person that I'm actually attracted to so I can confirm that

whenever I try to think about my sexuality I feel like I'm blindfolded and throwing darts at a board labeled with genders

Day 3 of learning Lean 4

Types are 2 Dimensional

that is all