But the subsequent paragraph talks about the truth of proofs themselves as being subjective.
This reflects the development of intuitionism. The project was first started by L. E. J. Brouwer, who rejected formalism. It was then developed by his student Arend Heyting, who formalized it with the Heyting algebra, a restricted variant of Boolean algebra that lacks the double negation elimination (~~p => p) and law of the excluded middle (p OR ~p).
Pretty much all work in intuitionistic mathematics continues the work of Heyting. Brouwer would have rejected the entire enterprise as subjective, so he is mainly of historical and philosophical interest.
This reflects the development of intuitionism. The project was first started by L. E. J. Brouwer, who rejected formalism. It was then developed by his student Arend Heyting, who formalized it with the Heyting algebra, a restricted variant of Boolean algebra that lacks the double negation elimination (~~p => p) and law of the excluded middle (p OR ~p).
Pretty much all work in intuitionistic mathematics continues the work of Heyting. Brouwer would have rejected the entire enterprise as subjective, so he is mainly of historical and philosophical interest.