In the proof of Bell's theorem of 1964, referenced e.g. here, the definition of a hidden variable seems to be any variable from which we can derive the correlation between the detectors, by calculating the integral over the values.
Isn't this what quantum mechanics already does? The wavefunction provides a spectrum that can then be integrated to obtain the correlation, where does one assume in the proof that the variable $\lambda$ is of some other "non-quantum" nature?
Bell's theorem assumes that the outcomes of the two measurements are $A(\vec a,λ)$ and $B(\vec b,λ)$ where $\vec a$ and $\vec b$ are the measurement settings, $λ$ is arbitrary "data" shared by the two particles, and $A$ and $B$ are arbitrary functions.
If you take $λ$ to be the wave function (plus a source of random bits to decide the outcomes of probabilistic measurements), and $A$ and $B$ to implement the measurement postulate of QM, you'll get the wrong answer. The reason is that you have to modify ("collapse") the wave function after each measurement, in a way that depends on the measurement, and feed the modified wave function into the next measurement. To fit that into Bell's framework, supposing wlog that you consider measurement A first, you'd have to say the measurement outcomes are $A(\vec a,λ)$ and $B(\vec b,λ')$ where $λ'$ is a function of $\vec a$ and $λ$, or equivalently that the outcomes are $A(\vec a,λ)$ and $B(\vec a,\vec b,λ)$. You can't prove Bell's inequality any more with that change.
the definition of a hidden variable seems to be any variable from which we can derive the correlation between the detectors,
The hidden variables referred to in the context of Bell's inequalities are usually local. A hidden variable theory limits itself to information available locally to avoid any requirement for FTL knowledge of states.
Let's say Alice and Bob are two spacelike separated observers with analysers whose orientation are defined by the vectors $\vec{a}$ and $\vec{b} $ respectively. The probability for the expected correlations' of their measurements is given by:
$$ P(\vec{a}, \vec{b}) = -\vec{a} \cdot \vec{b} $$
This QM prediction includes non local variables such as the orientation of the other observers analyser. A hidden variable theory has to make a prediction for the correlation $(-\vec{a} \cdot \vec{b}) \ $ measured by, for example, Bob without knowledge of the orientation of Alice's detector $\vec{a}$ at the instant Bob makes his measurement, which is impossible. The equation effectively becomes
$$ P(\vec{a}, \vec{b}) = -\text{?} \cdot \vec{b} $$
Bob could conspire with Alice to gain advance knowledge of the configuration of Alice's analyser. For example Alice could agree to always measure up spin. Now Bob can predict that if he make a simultaneous measurement for up spin, that the correlation should always be be zero, (i.e. always the opposite of what Alice measures at the instant Bob make his measurement). So the hidden local variables are the the orientation of Bob's analyser and the knowledge in his head of the orientation of Alice's analyser, but he still cannot predict the correct outcome for what he should measure without knowledge of the simultaneous measurement outcome made by Alice, which is classically impossible if they are spacelike separated. (By classical, I mean non-quantum behaviour).
"where does one assume in the proof that the variable λ is of some other "non-quantum" nature?" One assumes in the proof that any pair of observable quantities has a well-defined correlation, which is essentially tantamount to assuming that any pair of observable quantities can be simultaneously observed. This assumption is true of classical random variables, but false of quantum mechanical observables. Bell assumes that the hidden variables (such as $\lambda$) are classical (hence that the correlations are always well defined) and derives a contradiction with quantum mechanics (and with experiment).
In classical physics the evolution of each measurable quantity $x$ is described by a function $x(t)$ whose value is the same as the result you would get by measuring $x$.
I'm going to discuss quantum theory in the Heisenberg picture rather than the Schrodinger picture because the Heisenberg picture describes the evolution of physical quantities and individual systems more clearly than does the Schrodinger picture. I should also note that the account I will give here supposes that the equations of motion of quantum theory are an accurate description of how the world actually works and aren't modified by collapse or extra particles as in pilot wave theory. Collapse and extra particle assumptions contradict the equations of motion of quantum theory so I won't include them.
In quantum physics the evolution of a physical quantity $y$ is described by an observable $\hat{Y}(t)$ whose value is a Hermitian operator where the possible results of a measurement of $y$ are the eigenvalues of $\hat{Y}(t)$. Most observables have more than one eigenvalue and more than one possible measurement result. The evolution of $\hat{Y}(t)$ describes a process involving all of the possible values of $\hat{Y}(t)$. To make predictions one needs another Hermitian operator $\rho$ called the state which is a record of what measurements happened in the past and what outcomes you saw. The expectation value of measurements of $\hat{Y}(t)$ in the state $\rho$ is
$$\langle\hat{Y}(t)\rangle=tr(\rho\hat{Y}(t))$$
Suitable experiments such as single particle interference experiments can involve manipulating the projectors of $\hat{Y}(t)$ corresponding to each of the possible values in such a way that the expectation values depend on what happened to each of the possible values. For an example, see section 2 of this paper:
https://arxiv.org/abs/math/9911150
Note that the value of $\hat{Y}(t)$ at a given time is a matrix and the possible measurement results are the eigenvalues so the value of $\hat{Y}(t)$ is not the same as any of the possible measurement results, they aren't even the same kind of mathematical object.
A hidden variable would be a quantity $y(t)$ whose value at any given time time was the same as the outcome of measuring $y$. For something like the spin of an electron $y(t)$ would be either $+\tfrac{\hbar}{2}$ or $-\tfrac{\hbar}{2}$. The corresponding quantum observable would be $+\tfrac{\hbar}{2}$ times a matrix from a set of matrices satisfying the Pauli algebra, such as $$\frac{\hbar}{2}\begin{bmatrix} 1 & 0\\ 0 & -1 \end{bmatrix}$$
Unsurprisingly if you try to represent a quantity that is described by a Hermitian matrix by a single number instead the resulting theories contradict one another:
https://arxiv.org/abs/quant-ph/9906007
https://arxiv.org/abs/1109.6223
After you have done a measurement you only see a single outcome but that isn't because the outcome is described by a hidden variable. Rather, it is because interactions that produce copyable records of a measured quantity suppress interference, this is called decoherence:
https://arxiv.org/abs/quant-ph/0306072
This suppression of interference causes the different versions of the measurement device after the measurement to evolve independently of one another to a good approximation, this is often called the many worlds interpretation:
https://arxiv.org/abs/1111.2189
https://arxiv.org/abs/quant-ph/0104033
It should be noted that this approximation isn't perfect and the Bell correlations illustrate one way that this approximation can break down. The correspondence between measurement results on different systems only comes about after their measurement results are compared. Spatially separated systems are not yet divided into non-interfering relative states with respect to one another. For a description of local relative states see:
