While Curry-Howard is an insightful and beautiful result, this article doesn't currently explain it. By Curry-Howard, if I say that type T corresponds to proposition P, what I'm saying is "it's possible to create a value of type T if and only if P is true" (with the caveat that the program that creates type T neither crashes nor infinitely loops).

Let's take a look at the first example in the article:

type Integer = number;

// odd number is defined as 2x + 1
//  where x is an Integer
type OddNumber = {
  coefficient: 2,
  term: Integer,
  constant: 1,
}

// even number is defined as 2x
//  where x is an Integer
type EvenNumber = {
  coefficient: 2,
  term: Integer,
  constant: 0,
}

function addOdds(a: OddNumber, b: OddNumber): EvenNumber {
  // a + b
  // where a and b are odd numbers
  // = (2x + 1) + (2y + 1)
  // = 2x + 2x + 2
  // = 2(x + y + 1)

  // calculate (x + y + 1)
  const n = (a.term + b.term + 1) as Integer;
  // we get an integer n
  // we can put this in the form 2n to get an even number
  return {
    coefficient: 2,
    term: n,
    constant: 0,
  };
}

The key is addOdds, which takes two odds and returns an even. But I could just as easily write a function that takes two odds and returns an odd:

function addOdds(a: OddNumber, b: OddNumber): OddNumber {
  return {
    coefficient: 2,
    term: 1,
    constant: 1,
  };
  // Alternatively, we could just `return a`
}

Is this a proof that adding two odds results in an odd? Of course not: there's nothing in the type of addOdds that says anything about addition. There's no point in a proof system that can prove false things. All it proves is that, given two odd numbers, an odd number exists. If you want to prove that adding two odds results in an even, you have to include the concept of addition in your types.

One example of how to actually use Curry-Howard to prove things would be this tutorial in Idris, a language designed for more complex types: https://idris2.readthedocs.io/en/latest/proofs/inductive.html