The conjecture that the number of alternating sign matrices "bordered" by s is explicitly given by the formula

This conjecture was proved by Doron Zeilberger in 1995 (Zeilberger 1996a). This proof enlisted the aid of an army of 88 referees together with extensive computer calculations.
A beautiful, shorter proof was given later that year by Kuperberg (Kuperberg 1996),
and the refined alternating
sign matrix conjecture was subsequently proved by Zeilberger (Zeilberger 1996b)
using Kuperberg's method together with techniques from -calculus and orthogonal
polynomials.

Bressoud, D. Proofs and Confirmations: The Story of the Alternating Sign Matrix Conjecture. Cambridge,
England: Cambridge University Press, 1999.Bressoud, D. and Propp, J.
"How the Alternating Sign Matrix Conjecture was Solved." Not. Amer.
Math. Soc.46, 637-646.Finch, S. R. Mathematical
Constants. Cambridge, England: Cambridge University Press, p. 413, 2003.Kuperberg,
G. "Another Proof of the Alternating-Sign Matrix Conjecture." Internat.
Math. Res. Notes, No. 3, 139-150, 1996.Zeilberger, D. "A
Constant Term Identity Featuring the Ubiquitous (and Mysterious) Andrews-Mills-Robbins-Rumsey
numbers 1, 2, 7, 42, 429, ...." J. Combin. Theory A66, 17-27,
1994.Zeilberger, D. "Proof of the Alternating Sign Matrix Conjecture."
Electronic J. Combinatorics3, No. 2, R13, 1-84, 1996a. http://www.combinatorics.org/Volume_3/Abstracts/v3i2r13.html.Zeilberger,
D. "Proof of the Refined Alternating Sign Matrix Conjecture." New York
J. Math.2, 59-68, 1996b.