APL, 16 14 12 characters

Returns 0 for a leap year, 1 for a non-leap year.

≥/⌽×4 25 4⊤⎕

Try this solution on tryapl.com. Note that I have changed the solution to the dfn {≥/⌽×4 25 4⊤⍵} as tryapl.com does not support ⎕ (take user input). Note that ⎕ is an empty box, not a missing character.

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.

APL, 16 14 12 characters

Returns 0 for a leap year, 1 for a non-leap year.

≥/⌽×4 25 4⊤⎕

Try this solution on tryapl.org. Note that I have changed the solution to the dfn {≥/⌽×4 25 4⊤⍵} as tryapl.com does not support ⎕ (take user input). Note that ⎕ is an empty box, not a missing character.

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.

APL, 16 14 12 characters

Returns 0 for a leap year, 1 for a non-leap year.

≥/⌽×4 25 4⊤⎕

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.

APL, 16 14 12 characters

Returns 0 for a leap year, 1 for a non-leap year.

≥/⌽×4 25 4⊤⎕

Try this solution on tryapl.com. Note that I have changed the solution to the dfn {≥/⌽×4 25 4⊤⍵} as tryapl.com does not support ⎕ (take user input). Note that ⎕ is an empty box, not a missing character.

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.

APL, 16 14 characters

Returns 0 for a leap year, 1 for a non-leap year.

{≥/⌽×4 25 4⊤⍵}

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.

APL, 16 14 12 characters

Returns 0 for a leap year, 1 for a non-leap year.

≥/⌽×4 25 4⊤⎕

The same solution in J:

4 25 4>:/@|.@:*@#:]

Explanation

Dyadic ⊤ (encode) represents its right argument in the base specified by its left argument. I use base 4 25 4 in this solution. This represents the year y as a polynomial

y mod 400 = 100 a + 4 b + c where b < 100 and c < 4.

Let propositions α, β, and γ represent if a, b, and c are non-zero: Proposition γ is false if y is dividable by 4, β ∧ γ is false if y is dividable by 100 and α ∧ β ∧ γ is false if y is dividable by 400.

A truth table (* representing “don't care”) were proposition Δ represents if y is a leap-year obtains:

α β γ | Δ
0 0 0 | 1
1 0 0 | 0
* 1 0 | 1
* * 1 | 0

The following statement expresses Δ in α, β, and γ:

Δ = ¬((α → β) → γ)).

Due to the structure of this statement, one can express ¬Δ as the reduction ≥/⌽α β γ where ≥ implements ←. This leads to the answer I am explaining right now.