Is it possible for someone with little set-theoretic knowledge (e.g., me) to understand the proofs that either $\mathsf{CH}$ or $\mathsf{AC}$ is independent of $\mathsf{ZF}$?
I am looking for any kind of mathematical-sounding statement (not "This sentence is unprovable") for which the proof of independence is somewhat accessible.
On
The ability to understand the proof is one thing, and the ability to understand its details is another.$\newcommand{Dom}{\operatorname{dom}}\newcommand{Rng}{\operatorname{rng}}$
The point of independence proofs is to show that there can be a model in which the claim holds and another in which it does not hold (i.e. its negation holds).
For the general outline of the proof, there is a model of ZF in which AC and GCH hold as well. Given $M$ a model of ZF we have a way to create this model inside, usually marked as $L^M$. This shows that if there is a model of ZF (namely, ZF is consistent) then we have a model of ZF+AC+GCH.
For the other direction we use forcing. Forcing is a method in which we describe a certain object that does not necessarily exist within the original universe of ZF[C], but can be defined from our set of conditions.
The simplest example, I believe, is the Levy collapse of $\omega_1$ to $\omega$, which introduce into the world a bijection from $\omega$ to $\omega_1$ which means that we pulled an uncountable ordinal to be countable. We do this by approximating the function by finite terms, and claiming that by adding a certain set we can define from it a function which is bijective from $\omega$ onto $\omega_1$. (This is outlined further below)
In a sense this is complementary to the idea of adding $\sqrt{-1}$ to the real numbers to have $-1$ as a square. We add new objects to the universe and they witness some property.
To show the consistency of the negation of GCH, we add "enough" (that is more than $\aleph_1$) new subsets of natural numbers, making the continuum at least as big as the amount of sets we have added.
For the AC proof, this is somewhat more complicated as in general forcing extensions retain the original axioms, so one has to somehow create a submodel which extends the original model in which the axiom of choice does not hold. This is usually demonstrated by creating a countable set and in a sense leaving all the functions which well order it outside of the intermediate submodel.
I will outline the Levy collapse (which proves that being a cardinal number is not absolute) of $\omega_1$ to a countable ordinal:
Definition: Let $\langle P,<\rangle$ be a partially ordered set, $G\subseteq P$ is called a filter if:
Definition: If $\langle P,<\rangle$ is a poset, $D\subseteq P$ is called a dense set if for every $q\in P$ there exists $p\in D$ such that $q<p$.
A very important thing to pay attention to is that we are going to change models frequently enough, and we may have a model with more or less dense sets than before. Which brings us to the following definition:
Definition: Suppose $M$ is a model of ZFC and $\langle P,<\rangle\in M$ is a poset. $G\subseteq P$ is called $M$-generic filter if:
There are many equivalent definitions to being a generic filter, this is the most basic one and I will use it here.
Assume $M$ is a model of ZFC. We have that $\omega_1$ is uncountable. Define the following partially ordered set: $P=\{ f\colon \omega\to\omega_1\mid |\Dom(f)|<\omega\}$, that is all the finite functions into $\omega_1$.
We say that $f<g$ if $f\subseteq g$ (that is the domain of $f$ is a subset of the domain of $g$ and they agree on the domain of $f$).
Note that it means that if $f,g$ are compatible then $\Dom(f)\cap \Dom(g)$ is the maximal common domain of them both, and they agree on that domain.
Let $G$ be an $M$-generic filter, assume $f,g\in G$ then they are compatible by definition, suppose by contradiction that $f\nless g$ and vice versa, we have that there is some $n$ such that $f(n)\neq g(n)$, but since $G$ is closed downwards we have that $\{\langle n,f(n)\rangle\}, \{\langle n,g(n)\rangle\}\in G$ and those are incompatible. (Do note, I am slightly cheating here, but it is okay).
We have if so that $G$ is an increasing chain of functions. Its union, by that property, is a function. We will call it the generic function $F=\bigcup G$, and this function lives in any universe in which both $M$ and $G$ exists, we denote it as $M[G]$.
Claim: In $M[G]$ the ordinal that was $\omega_1$ in $M$ (denoted as $\omega_1^M$) is countable.
Proof: We show that $F$ is a bijection from $\omega$ onto $\omega_1^M$. In $M$, for every $\alpha$ the set of functions $D_\alpha = \{f\in P\mid \alpha\in \Rng(f)\}$ is dense, as for every function $f\in P$ we can define $n_f = \min\{n\in\omega\mid n\notin \Dom(f)\}$ and define $f' = f\cup\{\langle n_f,\alpha\rangle\}$.
By genericity of $G$ we have that $G\cap D_\alpha\neq\emptyset$, that is $\alpha\in \Rng(F)$, however this happens for every $\alpha<\omega_1$.
By a similar argument we have that all $\omega$ is the domain of the function $F$.
This conclude the proof of how we collapsed $\omega_1$ from being uncountable to being countable.
Clearly $F$ and $G$ do not exist in $M$, as $M$ thinks of $\omega_1^M$ as uncountable. In a sense you need to think of it as though they exist in a bigger universe. Just like $\sqrt{-1}$ doesn't live in the real numbers, but exists in the complex numbers. The philosophy behind this argument is not easy, as comes the question "Why is there a generic filter at all?" which I cannot really answer, but can direct you to this MO answer which sheds some light on the topic.
A few notes, I did my best to avoid many of the needed technical lemmas and gave a straightforward forcing argument. In whole, forcing gets more and more technical as you progress onwards and it is nearly impossible to comprehend it without some extensive study - at least of the basics. I would be glad to clarify points in the example, or add more.
On
Here is a large class of very quick independence proofs, although they are not set-theoretic.
Suppose that $A$ is any computably enumerable set that is not computable. Thus, we have an algorithm to enumerate the elements of $A$, but there is no algorithm to enumerate the elements not in $A$. For example, the halting problem is like this, since we can enumerate the halting instances, but not the non-halting instances.
It follows that for infinitely many numbers $n$, the question of whether $n\notin A$ is independent of your favorite true and computably axiomatizable theory. For example, if there were no such $n$, then we would be able to decide $n\in A$ by waiting for $n$ to be enumerated into $A$ and simultaneously looking for a proof that $n\notin A$, contradicting that $A$ is not decidable.
In particular, non-membership in any c.e. non-decidable set is loaded with independent statements.
On
If you're willing to drop from ZF(C) down to PA - that is, settle for arithmetic rather than sets - then I believe Goodstein's Theorem (or slightly more complicatedly, the Paris-Harrington theorem) might be what you're after; both of these are relatively straightforward statements of arithmetic. The proofs of independence are unfortunately still fairly complicated and full of technical details, but the core concept ('Peano Arithmetic isn't strong enough to prove induction principles past a certain point') may be more straightforward to grok than the mechanics of forcing and building models of set theory.
As far as forcing itself goes, I think the most amateur-friendly approach may be through modal logic; I'm a great fan of Smullyan and Fitting's Set Theory and the Continuum Problem. It has its share of (mostly printing) flaws, but it's really quite accessible and covers the material well. You might want Smullyan's more casual Forever Undecided (if you can find it!) as a warm-up; it goes over some of the basics of modal logic in a puzzle-oriented setting.
While I can't say what you personally will or will not be able to understand, forcing (the method that one uses to show that one set of axioms is independent from another set) is a powerful idea which many people have written about and tried to make accessible. If you search google for something like "introduction to forcing" you will find a few such guides (and a few things having nothing to do with logic). For example, this or this. Worst case scenario, if those don't make sense, you will at least be exposed to the ideas that you will have to familiarize yourself with. In particular, you will probably want to at least look at the wikipedia page on model theory.