I’d like to share these spectacular images of our Sun, taken by Prasad Agrahar with his home-made spectroheliograph.
His first image is at H-alpha (656 nm), second is at H-beta (486 nm), and the third is at Helium D3 (585 nm).
With this device, IIUC, he can make an image at just about any wavelength that makes it through the front lens of the optics. He posted this to the NCA email list.
DIY!!
Guy Brandenburg
Prasad wrote:
Here are three images of our Sun, taken on Thursday morning with my DIY spectroheliograph. The weather was quite windy, and the seeing was poor.
The above is H-alpha with [sunspot groups] AR 4294 and 4296 dazzling.
This is H-beta
And finally,
The above image is (…) Helium-D3, the emission line at 5875A.
Dr Rob Zellem posed this question last night (9-13-2025) to NCA members and visitors at their monthly meeting at the University of Maryland Observatory.
Are we alone in the universe, or are there exoplanets with life of some sort, and even some advanced civilizations out there?
Dr Zellem said the correct answer right now is, maybe. We just don’t have enough data to tell.
He reminded us that Giordano Bruno and Isaac Newton both correctly predicted that other stars would have planets around them. We now know that just about every single star is born with a retinue of planets, asteroids, dust, and comets, so there are at least as many planets as there are stars in our galaxy and all the others as well. Previous speakers to NCA have noted that many of these objects end up getting flung out into the vast frozen emptiness of interstellar space in a giant random game of ‘crack the whip’. No life can exist out there.
My calculations here: It is estimated that there are literally trillions (10^12) of galaxies, each with millions (10^6) or billions (10^9) of stars. Let’s start with our own galaxy, the Milky Way, with maybe 200 billion stars (maybe more). I will assume that life needs a nice, calm, long-lived G class yellow star, which only make up 7.6% of all stars. Roughly 50% to 70% of those stars are in binary systems, which I fear will reduce the chances of having a planet survive in the Goldilocks zone. Perhaps one-third to two-thirds of those G stars have a planet in their habitable zone. We have no idea how likely life is to get started, but after reading Nick Lane’s The Vital Question it sounds pretty complicated to me, so I’ll use a range of estimates: somewhere between 10% and 80% of them develop some form of life. We know that on Earth, the only form of life that existed during the vast majority of the existence of the Earth was unicellular microbes. Four-footed tetrapods like ourselves have only occupied about 1% of the life of our planet, and we humans have only had the telescope for just over 400 years, out of the 400,000,000 years since four-footed animals evolved, which is one in a million. Low estimate:
If my low-end estimates are correct, then there are about five or so exo-planets somewhere in our galaxy with a civilization formed by some sort of animal that can look out into outer space. High estimate:
In that case, there are well over a hundred civilizations in our galaxy — but the Milky Way is huge, hundreds of thousands of light-years across! Most of our exoplanet detections have been within the nearest 100 light years, and we have no way of detecting most exoplanets at all because the planes of their orbits point the wrong way.
NOTE: Jim Kaiser pointed out that I made a dumb mistake: a hundred billion is ten to the 11th power, not ten to the 14th power. Fixed now.
Even so, Zellem pointed out that thanks to incredible advances in sensitivity of telescopes and cameras, we are now closer than ever to being able to answer the title question: Are We Alone.
Plus, any amateur astronomer can take useful measurements of exoplanet transits with any telescope, and any digital camera. Following the directions on NASA’s Planet Watch webpage, you can take your data, in your back yard or from a remote observatory, process it the best you can, send it in, and be credited as a co-author on any papers that are published about that particular exoplanet. Then, later, a massive space telescope can be aimed at the most promising exoplanets during their transits. Astronomers can use their extremely sensitive spectroscopes to detect the atmospheres of those bodies and look for signs of life. They do not want to waste extremely valuable telescope time waiting for a transit that doesn’t recur!
Some day we will be in a situation where scientists will be able to say that based on their measurements, the signal indicates a very good chance of life at least a bit like ours, with similar chemistry on some planet. They will also state what the chances are that they are wrong, and indicate what further steps could be made to disprove or confirm their claim.
Zellem noted that both the Doppler-shift method and the transit methods are quite biased in favor of large exoplanets that are close to their suns.
I asked the speaker how likely it would be for observers from some exoplanet to detect the planet Mercury, but couldn’t do the math in my head and didn’t have paper and pencil to write anything down at the time. But now I do.
The closer Mercury is to the Sun, the larger the possible viewing angle.
Using a calculator to find the arc-tangent of that ratio (865,000 miles solar diameter, divided by the smallest and also by the largest distances between them, namely 28,500,000 and 43,500,000 miles) gave me an angle between 2 and 3 degrees, depending. So there is a circular wedge of our galaxy where observers on some other planet might view a transit of our innermost planet. Where is that wedge in our galaxy?
The following sky diagram has the Ecliptic in pink. Only observers within a degree or so of that curvy line could detect that Sol has planets.
So what fraction of the sky can ever hope to catch a transit of Mercury? Only about 1% or 2% of the sky — not much.
Turning things around, this means that we can ourselves only detect, via transits, a very small portion of all extra-solar planetary systems – those whose planes are pointing almost directly at us, and those with large planets that are very close to their stars. (Any planet so close to a star is not a very good candidate for life, in my opinion.)
The biggest obstacle is the sheer distances between stars. At the speed of our very fastest space craft (the Parker Solar Probe), which only goes 0.064% of the speed of light, it would take about 6250 years to reach our closest stellar neighbors near Proxima Centauri. One way. Which probably explains why, if all these other civilizations do exist, we do not appear so far to have been visited by any other extraterrestrial civilization.
At the meeting, someone in the audience was pretty sure that yes, we have already been visited by aliens. I talked with him outside after the meeting. His main evidence was a 2020 New York Times article concerning the upcoming release of classified data about mysterious flying objects (now called UAPs rather than UFOs). In the article, one Eric Davis claimed (without producing any evidence) that some items have been retrieved from various places by the US military that couldn’t be made here on earth. That is of course true of every single asteroid or meteorite ever discovered, since we can’t reproduce the conditions in which they were formed, so his claim is not very helpful. No technological devices clearly of alien manufacture have ever been publicly produced by him or anybody else for testing.
(It’s pretty obvious that American and other military forces spend a lot of money producing objects that go very fast and are highly maneuverable — and which they want to keep secret.)
There are in fact many, many unsolved mysteries in science (eg, the nature of dark matter and dark energy, and exactly how the nucleus arose in eukaryotes). Many of the unidentified sky or water phenomena that have been witnessed do not have clear explanations so far, but the simplest explanation is usually the correct one. Reputable scientists require a lot more than hearsay evidence before they make bold claims.
Last night was the opening of an exhibit called Second Sunset in an alley off Mt Pleasant Triangle in NW DC. Great astrophotos by 19-year old Gael Gomez, his neighbor Adam Green, and NCA VP Bryan Vandrovec! The images are huge – four to six feet across, and printed on durable sandwiches of aluminum and plastic, so they will survive outside for months. They were printed by Jason Hamacher of Lost Origins Gallery, located about a block away, aided in part by the Smithsonian’s Folk Life Festival.
It coincided with the 3rd annual Art All Night – Mount Pleasant, so a LOT of people were out having a good time, listening to a live Colombian band and visiting dozens of vendors and exhibits under tent covers on the Triangle.
So when Gael and Guy Brandenburg (NCA president) brought out their telescopes on the other side of Mt Pleasant Street, once we could actually see a few stars, we had long lines of people waiting patiently to look at double stars, Saturn, the ISS, and the Moon, and then discussing what they had seen, right up until 11:30 PM. We all had a blast!
If you can’t read the text, it says, “The Art of DIY Telescopes, Sidewalk Astronomy, and Astrophotography: The Debut Exhibit of the Mt Pleasant Sidewalk Astronomers”. As well as “Lost Origins Outside” and “November 12 to November 9, 2025.”
Captions are coming for all of the photos, explaining how they were made and what they depict, as well as a sign explaining the National Capital Astronomers which has been running the DC DIY telescope workshop since World War 2, in which both Guy and Gael made their first telescopes.
We only truly discovered the nature of galaxies, of nuclear fusion, and of the scale of the universe a mere century ago.
Dark matter was discovered by Vera Rubin just over 40 years ago and dark energy a few years later, just before the time that both professional and amateur astronomers began switching over to CCD and later CMOS sensors instead of film
The first exoplanet was discovered only 30 years ago, and the count is now up to almost six thousand of them (as of 1/21/2024).
While multi-billion dollar space telescopes and giant observatories at places like Mauna Kea and the Atacama produce the big discoveries, amateur astronomers with a not-outrageous budget can now afford to purchase relatively small rigs armed with excellent optics and complete computer control, and lots of patience and hard work, can and so produce amazing images like the ones here https://www.novac.com/wp/observing/member-images/ or this one https://www.instagram.com/gaelsastroportrait?igsh=cjMzYWlqYjNzaDlw, by one of the interns on this project. Gael’s patience, cleverness, dedication and follow-through are all praiseworthy.
However, it is getting harder and harder every year for people to see anything other than the brightest planets, because of ever-increasing light pollution; the vast majority of the people in any of the major population centers on any continent have no hope of seeing the Milky Way from their homes unless there is a wide-spread power outage. Here in the US, such power outages are rare, which means that if you want to go out and find a Messier object, you pretty much cannot star-hop, because you can only see four to ten stars in the entire sky!
One choice is to buy a completely computer-controlled SCT like the ones sold by Celestron. They aren’t cheap, but they will find objects for you.
But what if you don’t want another telescope, but instead want to give nice big Dobsonian telescope the ability to find things easily, using the capabilities inside one’s cell phone?
Some very smart folks have been working on this, and have come up with some interesting solutions. When they work, they are wonderful, but they sometimes fail for reasons not fully understood. I guess it has something to do with the settings in the cell phone being used.
The rest of this will be on one such solution, a commercial one called StarSense from Celestron that holds your phone in a fixed position above a little mirror, and you aim the telescope and your cell phone’s camera at something like the top of a tower far away. Then it uses both the interior sensors on your cell phone and images of the sky to figure out where in the sky your scope is pointing, and tells you which way to push it to get to your desired target.
When it works, it’s great. But it sometimes fails.
You have to buy an entire set from Celestron – one of their telescopes (which has the gizmo built in) along with the license code to unlock the software.
You supply the cell phone.
The entire setup ranges in price from about $200 to about $2,000. You cannot just buy the holder and the code from them; you must buy a telescope too. I already had decent telescopes, which I had made, so I bought the lowest-priced one. I then unscrewed the plastic gizmo, and carved and machined connection to a male dovetail slide for it. I also fastened a corresponding female dovetail to each of my scopes. The idea was to then slip this device off or onto whichever one of my telescopes is going to get used that night, as long as I that has a vixen dovetail saddle, and put inexpensive saddles on several scopes I have access to.
Here are some photos of the gizmo:
NCA’s current interns (Nabek Ababiya and Gael Gomez) and I were wondering about the geometry of the angles at which StarSense would aim at the sky in front of the scope. My guess had been that Celestron’s engineers would make the angles of their device so that the center of the optical pencil hitting the lens dead-on at 90 degrees, and hence coning to a focus at the central pixel of the CMOS sensor, would be parallel to the axis of the telescope tube.
We didn’t want to touch the mirror, because it’s quite delicate. But as a former geometry teacher, I couldn’t leave this one alone, so along with Gael and Nabek I made some diagrams and figured out what the angles had to be if the axis of the StarSense app’s image were designed to be precisely parallel to the axis of the telescope.
In my diagram below, L is the location of the Lens, and IJCK is the cell phone lying snug in its holder. The user can slide the cell phone left and right along that line JD as we see it here, or into out of the plane of the page, but it is not possible to change angle D aka <CDE – it’s fixed by the factory molds to be some fixed angle that we measured with various devices to be 19.0 degrees.
Here is a version of the diagrams we made that showed what we predicted all the angles would be so that optical axis OH will be parallel to the tube axis EBD, and that lens angle ILH is a right angle. We predicted that the mirror’s axis would need to be tilted upwards by an angle of 35.5 degrees (anle HBD).
To our surprise, our guesses and calculations were all wrong!
After careful measurements we found that Celestron’s engineers apparently decided that the optical axis of the SS gizmo should instead aim the cell phone’s camera up by 15.0 degrees (angle BGH below). The only parallel lines are the sides of the telescope tube!
We used a variety of devices to measure angle FBD and MNC to an accuracy of about half a degree; all angles turned out to be whole numbers.
Be that as it may, sometimes it works well and sometimes it does not.
Zach Gleiberman and I tested it on an open field in Rock Creek Park here in DC back in the fall of 2024, using the Hechinger-blue 8 inch dob I made 30 years ago and still use. We found that SS worked quite well, pointing us quite accurately to all sorts of targets using my iPhone SE. The sky was about as good as it gets inside the Beltway, and the device worked flawlessly.
Not too long afterwards, I decided to try out an Android-style phone (a REVVL 6 Pro) so that I wouldn’t have to give up my cell phone for the entire evening at Hopewell Observatory. I was unpleasantly surprised to find that it didn’t work well at all: the directions were very far off. I thought it might be because the scope in question had a rather wide plywood ring around the front of its very long tube, and that perhaps too much of the field of view was being cut off?
Why it fails was not originally clear. I thought nearly every modern phone would work, since for Androids, it just needs to be later than 2016 and have a camera, an accelerometer, and gyros, which is a pretty low bar these days. However, my REVVL 6 Pro from T-Mobile is not on the list of phones that have been tested to work!
Part of my assumption that the axis of the SS gizmo would be parallel to the axis of the scope was an explanation that StarSense on had such a large obstruction in front of the SS holder, in the form of a wide wooden disk reinforcing the front of a 10″ f/9 Newtonian, that the SS was missing part of the sky. We now know that’s not correct. It’s an interface problem (ie software) problem.
Come to Bull Run Mountain for a free night under the stars looking at a variety of targets using the telescopes at the Hopewell Observatory on Saturday, April 27, 2024.
You are invited, but will need to RSVP and, in this litigious age, must agree to a waiver of liability for anything that might happen out there in the woods – and they do exist! Plus we don’t have running water — so, we use an outhouse.
But if you take the risk you, for free, can view Jupiter and its moons, comet 12P/Pons–Brooks, and a bunch of bright open clusters like the Pleiades, Beehive and Orion star clusters — and a gaggle of galaxies and double stars.
We have a variety of permanently-mounted and portable telescopes of different designs, some commercial and some made by us, some side-by-side, enabling several people to view the same object in the sky with different magnifications.
The date is Saturday, April 27. We suggest arriving near sundown, which will happen near 8 pm. It will get truly dark about an hour later.
There are no street lights near our observatory, other than some dimly illuminated temporary signs we put along the path, so you will probably want to bring a flashlight of some sort.
If you own a scope or binoculars, feel free to bring them!
Hopewell is about 45 minutes by car from where I-66 intersects the DC beltway. The last two miles of road are dirt and gravel, and you will need to walk about 200 meters/yards from where you park. We do have electricity, and a heated cabin, but since we have no running water, we have an outhouse and hand sanitizer instead.
We are located about 30 miles west of the Beltway on Bull Run Mountain – a ridge that overlooks Haymarket VA from an elevation of 1100 feet, near the intersection of I-66 and US-15. Detailed directions are below.
Assuming good weather, you’ll also get to see the Milky Way itself, although not as well as in years past, because of ever-increasing light pollution.
If you like, you can bring a picnic dinner and a blanket or folding chairs, and/or your own telescope binoculars, if you own one and feel like bringing them. We have outside 120VAC power, if you need it for your telescope drive, but you will need your own extension cord and plug strip. If you want to camp out or otherwise stay until dawn, feel free!
If it gets cold, our Operations Building, about 40 meters north of the Observatory itself, is heated, and we will have the makings for tea, cocoa, and coffee.
Warning: While we do have bottled drinking water and electricity and we do have hand sanitizer, we do not have running water; and, our “toilet” is an outhouse of the composting variety. At this time of year, the bothersome insects haven’t really taken off but feel free to use your favorite bug repellent, (we have some) and check yourself for ticks after you get home.
The road up here is partly paved, and partly gravel or dirt. It’s suitable for any car except those with really low clearance, so leave your fancy sports car (if any) at home. Consider car-pooling, because we don’t have huge parking lots.
Two of our telescope mounts are permanently installed in the observatory under a roll-off roof. One is a high-end Astro-Physics mount with a 14” Schmidt-Cassegrain and a 5” triplet refractor. The other was manufactured about 50 years ago by a firm called Ealing, but the motors and guidance system were recently completely re-done by us with modern electronics using a system called OnStep. We didn’t spend much cash on it, but it took us almost a year to solve a bunch of mysteries of involving integrated circuits, soldering, torque, gearing, currents, voltages, resistors, transistors, stepper drivers, and much else.
We could not have completed this build without a lot of help from Prasad Agrahar, Ken Hunter, the online “OnStep” community, and especially Arlen Raasch. Thanks again!
OnStep is an Arduino-based stepper-motor control system for astronomical telescopes. For this niche application, OnStep uses very inexpensive, off-the-shelf components such as stepper motors and their controller chips — which were developed previously for the very widespread 3-D printing and CNC machining industry.
Getting this project to completion took us nearly a full year of hard work!!! The original, highly accurate Byers gears are still in place, but now we can control the mount from a smart phone!
We also have two alt-az telescopes, both home-made (10” and 14”) that we roll out onto our lawn, and a pair of BIG binoculars on a parallelogram mount.
The drive is about an hour from DC. After parking at a cell-phone tower installation, you will need to hike south about 200 meters/yards to our observatory.
Physically handicapped people, and any telescopes, can be dropped off at the observatory itself, and then the vehicle will need to go back to park near that tower. To look through some of the various telescopes you will need to climb some stairs or ladders, so keep that in mind when making your plans.
Our location is nowhere near the inky dark of the Chilean Atacama or the Rockies, but Hopewell Observatory is mostly surrounded by nature preserves maintained by the Bull Run Mountain Conservancy and other such agencies. Also, our Prince William and Fauquier neighbors and officials have done a fair job of insisting on smart lighting in the new developments around Haymarket and Gainesville, which benefits everybody. So, while there is a bright eastern horizon because of DC and its VA suburbs, we can still see the Milky Way whenever it’s clear and moonless. “Clear Outside” says our site is Bortle 4 when looking to our west and Bortle 6 to our east.
DIRECTIONS TO HOPEWELL OBSERVATORY:
[Note: if you have a GPS navigation app, then you can simply ask it to take you to 3804 Bull Run Mountain Road, The Plains, VA. That will get you very close to step 6, below.]
(1) From the Beltway, take I-66 west about 25 miles to US 15 (Exit 40) at Haymarket. At the light at the end of the ramp, turn left (south) onto US 15.
(2) Go 0.25 mi; at the second light turn right (west) onto VA Rt. 55. There is a Sheetz gas station & convenience store at this intersection, along with a CVS and a McDonald’s. After you turn right, you will pass a Walmart-anchored shopping center on your right that includes a number of fast- and slow-food restaurants. After that you will pass a Home Depot on the right.
(3) After 0.7 mi on Va 55, turn right (north) onto Antioch Rd., Rt. 681, opposite a brand-new housing development. You will pass entrances for Boy Scouts’ Camp Snyder and the Winery at La Grange.
(4) Follow Antioch Rd. to its end (3.2 mi), then turn left (west) onto Waterfall Rd. (Rt. 601), which will become Hopewell Rd after you cross the county line.
(5) After 1.0 mi, bear right (north) onto Bull Run Mountain Rd., Rt. 629. This will be the third road on the right, after Mountain Rd. and Donna Marie Ct. (Do NOT turn onto Mountain Road, and note that some apps show a non-existent road, actually a power line, in between Donna Marie Ct. and Bull Run Mtn. Rd.) Bull Run Mtn Rd starts out paved but then becomes gravel, and rises steadily.
(6) In 0.9 mi, on BRMtn Road, you will see a locked stone gate and metal gate, labeled 3804. That is not us! Instead, note the poorly-paved driveway on the right, with the orange pipe gate swung open and a sign stating that this is an American Tower property. We use their road. Drive through both orange gates, avoiding potholes keeping at least one tire on the high spots. We’ll have some signs up. This is a very sharp right hand turn.
(7) Follow the narrow, poorly-paved road up the ridge to the cell phone tower station.
(8) Park your vehicle in any available spot near that tower or in the grassy area before the wooden sawhorse barrier. Then follow the signs and walk, on foot, the remaining 300 yards along the grassy dirt road, due south, to the observatory. Be sure NOT to block the right-of-way for any vehicles.
(9) If you are dropping off a scope or a handicapped person, move the wooden barrier out of the way temporarily, and drive along the grassy track to the right of the station, into the woods, continuing south, through (or around) a white metal bar gate. (The very few parking places among the trees near our operations cabin, are reserved for Observatory members and handicapped drivers.) If you are dropping off a handicapped person or a telescope, afterwards drive your car back and park near the cell phone tower.
Please watch out for pedestrians, especially children!
In the operations cabin we have a supply of red translucent plastic film and tape and rubber bands so that you can filter out everything but red wavelengths on your flashlight. This will help preserve everybody’s night vision.
The cabin also have holds a visitor sign-in book; a first aid kit; a supply of hot water; the makings of hot cocoa, tea, and instant coffee; hand sanitizer; as well as paper towels, plastic cups and spoons.
The location of the observatory is approximately latitude 38°52’12″N, longitude 77°41’54″W. The drive takes about 45 minutes from the Beltway. A map to the site follows. If you get lost, you can call me on my cell phone at 202 dash 262 dash 4274.
An alarming article about studies of bird deaths due to bright city lighting. A couple of quotes:
Every 11 September at dusk, in memory of the 2001 attacks, New York City mounts the Tribute in Light, an art installation in lower Manhattan. And every year, as twin towers of light bloom skyward, they attract thousands of migrating birds, sucking in warblers, seabirds, and thrushes—along with predators such as peregrine falcons eager to take advantage of the confusion. On each anniversary, bird conservationists wait below, counting and listening to disoriented chirps. If the observers report too many birds circling aimlessly in the beams, organizers flip off the lights.
In recent years, on-site observers have also used a complementary tool to quantify the orbiting birds: weather radar, which bounces off birds as well as raindrops. In 2017, a group led by Cornell University ornithologist Andrew Farnsworth found that during seven previous anniversaries, the once-a-year installation had attracted a total of about 1.1 million birds. Within 20 minutes of lighting up, up to 16,000 birds crammed themselves into a half-kilometer radius. But when the lights flicked off, the dense clouds of birds on the radar screen dissipated just as fast, a finding later confirmed by on-site thermal cameras.’
Later, discussing a single building, the author found that a
‘key factor was how many of the convention center’s windows had been illuminated. Each individual bright window left more dead birds for volunteers to find the next day. The correlation suggests halving the number of lit window bays would halve the number of bird strikes, the team estimated, saving thousands of birds at this one three-story building. “It really does seem that each window makes a difference,” van Doren says.’
Can they ever be? From reading this article and my own experience with the geometry-proving-and-construction software called Geometrix, written by my friend and colleague Jacques Gressier, I am not sure it’s possible at all.
Here is an interesting article that I’m copying and pasting from Jerry Becker at SIU, who got it from Quanta:
How Close Are Computers to Automating Mathematical Reasoning?
AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.
By Stephen Ornes
In the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made a sweeping prediction that continues to excite and irritate mathematicians – that “at some unspecified future time, mathematicians would be replaced by computers.” Cohen, legendary for his daring methods in set theory, predicted that all of mathematics could be automated, including the writing of proofs.
A proof is a step-by-step logical argument that verifies the truth of a conjecture, or a mathematical proposition. (Once it’s proved, a conjecture becomes a theorem.) It both establishes the validity of a statement and explains why it’s true. A proof is strange, though. It’s abstract and untethered to material experience. “They’re this crazy contact between an imaginary, nonphysical world and biologically evolved creatures,” said the cognitive scientist Simon DeDeo of Carnegie Mellon University, who studies mathematical certainty by analyzing the structure of proofs. “We did not evolve to do this.”
Computers are useful for big calculations, but proofs require something different. Conjectures arise from inductive reasoning – a kind of intuition about an interesting problem – and proofs generally follow deductive, step-by-step logic. They often require complicated creative thinking as well as the more laborious work of filling in the gaps, and machines can’t achieve this combination.
Computerized theorem provers can be broken down into two categories. Automated theorem provers, or ATPs, typically use brute-force methods to crunch through big calculations. Interactive theorem provers, or ITPs, act as proof assistants that can verify the accuracy of an argument and check existing proofs for errors. But these two strategies, even when combined (as is the case with newer theorem provers), don’t add up to automated reasoning.
——————-
SIDEBAR PHOTO: Simon DeDeo of Carnegie Mellon helped show that people and machines seem to construct mathematical proofs in similar ways. Courtesy of Simon DeDeo
——————–
Plus, the tools haven’t been met with open arms, and the majority of mathematicians don’t use or welcome them. “They’re very controversial for mathematicians,” DeDeo said. “Most of them don’t like the idea.”
A formidable open challenge in the field asks how much proof-making can actually be automated: Can a system generate an interesting conjecture and prove it in a way that people understand? A slew of recent advances from labs around the world suggests ways that artificial intelligence tools may answer that question. Josef Urban at the Czech Institute of Informatics, Robotics and Cybernetics in Prague is exploring a variety of approaches that use machine learning to boost the efficiency and performance of existing provers. In July, his group reported a set of original conjectures and proofs generated and verified by machines. And in June, a group at Google Research led by Christian Szegedy posted recent results from efforts to harness the strengths of natural language processing to make computer proofs more human-seeming in structure and explanation.
Some mathematicians see theorem provers as a potentially game-changing tool for training undergraduates in proof writing. Others say that getting computers to write proofs is unnecessary for advancing mathematics and probably impossible. But a system that can predict a useful conjecture and prove a new theorem will achieve something new – some machine version of understanding, Szegedy said. And that suggests the possibility of automating reason itself.
Useful Machines
Mathematicians, logicians and philosophers have long argued over what part of creating proofs is fundamentally human, and debates about mechanized mathematics continue today, especially in the deep valleys connecting computer science and pure mathematics.
For computer scientists, theorem provers are not controversial. They offer a rigorous way to verify that a program works, and arguments about intuition and creativity are less important than finding an efficient way to solve a problem. At the Massachusetts Institute of Technology, for example, the computer scientist Adam Chlipala has designed theorem-proving tools that generate cryptographic algorithms – traditionally written by humans – to safeguard internet transactions. Already, his group’s code is used for the majority of the communication on Google’s Chrome browser.
——————-
SIDEBAR PHOTO: Emily Riehl of Johns Hopkins University uses theorem provers in teaching students and proof assistants in her own work. “Using a proof assistant has changed the way I think about writing proofs,” she said. Will Kirk/Johns Hopkins University
———————-
“You can take any kind of mathematical argument and code it with one tool, and connect your arguments together to create proofs of security,” Chlipala said.
In math, theorem provers have helped produce complicated, calculation-heavy proofs that otherwise would have occupied hundreds of years of mathematicians’ lives. The Kepler conjecture, which describes the best way to stack spheres (or, historically, oranges or cannonballs), offers a telling example. In 1998, Thomas Hales, together with his student Sam Ferguson, completed a proof using a variety of computerized math techniques. The result was so cumbersome – the results took up 3 gigabytes – that 12 mathematicians analyzed it for years before announcing they were 99% certain it was correct.
The Kepler conjecture isn’t the only famous question to be solved by machines. The four-color theorem, which says you only need four hues to color any two-dimensional map so that no two adjoining regions share a color, was settled in 1977 by mathematicians using a computer program that churned through five-colored maps to show they could all be reduced to four. And in 2016, a trio of mathematicians used a computer program to prove a longstanding open challenge called the Boolean Pythagorean triples problem, but the initial version of the proof was 200 terabytes in size. With a high-speed internet connection, a person could download it in a little over three weeks.
Complicated Feelings
These examples are often trumpeted as successes, but they’ve also added to the debate. The computer code proving the four-color theorem, which was settled more than 40 years ago, was impossible for humans to check on their own. “Mathematicians have been arguing ever since whether or not it’s a proof,” said the mathematician Michael Harris of Columbia University.
———————-
SIDEBAR PHOTO: Many mathematicians, like Columbia University’s Michael Harris, disagree with the idea that computerized theorem provers are necessary – or that they’ll make human mathematicians obsolete. Béatrice Antolin
———————–
Another gripe is that if they want to use theorem provers, mathematicians must first learn to code and then figure out how to express their problem in computer-friendly language – activities that detract from the act of doing math. “By the time I’ve reframed my question into a form that could fit into this technology, I would have solved the problem myself,” Harris said.
Many just don’t see a need for theorem solvers in their work. “They have a system, and it’s pencil and paper, and it works,” said Kevin Buzzard, a mathematician at Imperial College London who three years ago pivoted his work from pure math to focus on theorem provers and formal proofs. “Computers have done amazing calculations for us, but they have never solved a hard problem on their own,” he said. “Until they do, mathematicians aren’t going to be buying into this stuff.”
But Buzzard and others think maybe they should. For one thing, “computer proofs may not be as alien as we think,” DeDeo said. Recently, together with Scott Viteri, a computer scientist now at Stanford University, he reverse-engineered a handful of famous canonical proofs (including one from Euclid’s Elements) and dozens of machine-generated proofs, written using a theorem prover called Coq, to look for commonalities. They found that the networked structure of machine proofs was remarkably similar to the structure of proofs made by people. That shared trait, he said, may help researchers find a way to get proof assistants to, in some sense, explain themselves.
“Machine proofs may not be as mysterious as they appear,” DeDeo said.
Others say theorem provers can be useful teaching tools, in both computer science and mathematics. At Johns Hopkins University, the mathematician Emily Riehl has developed courses in which students write proofs using a theorem prover. “It forces you to be very organized and think clearly,” she said. “Students who write proofs for the first time can have trouble knowing what they need and understanding the logical structure.”
————————–
SIDEBAR: By the time I’ve reframed my question into a form that could fit into this technology, I would have solved the problem myself. Michael Harris, Columbia University
————————-
Riehl also says that she’s been increasingly using theorem provers in her own work. “It’s not necessarily something you have to use all the time, and will never substitute for scribbling on a piece of paper,” she said, “but using a proof assistant has changed the way I think about writing proofs.”
Theorem provers also offer a way to keep the field honest. In 1999, the Russian American mathematician Vladimir Voevodsky discovered an error in one of his proofs. From then until his death in 2017, he was a vocal proponent of using computers to check proofs. Hales said that he and Ferguson found hundreds of errors in their original proof when they checked it with computers. Even the very first proposition in Euclid’s Elements isn’t perfect. If a machine can help mathematicians avoid such mistakes, why not take advantage of it? (The practical objection, justified or not, is the one suggested by Harris: If mathematicians have to spend their time formalizing math to be understood by a computer, that’s time they’re not spending doing new math.)
But Timothy Gowers, a mathematician and Fields medalist at the University of Cambridge, wants to go even further: He envisions a future in which theorem provers replace human referees at major journals. “I can see it becoming standard practice that if you want your paper to be accepted, you have to get it past an automatic checker,” he said.
————-
But before computers can universally check or even devise proofs, researchers first have to clear a significant hurdle: the communication barrier between the language of humans and the language of computers.
Today’s theorem provers weren’t designed to be mathematician-friendly. ATPs, the first type, are generally used to check if a statement is correct, often by testing possible cases. Ask an ATP to verify that a person can drive from Miami to Seattle, for example, and it might search all cities connected by roads leading away from Miami and eventually finding a city with a road leading into Seattle.
———————–
SIDEBAR PHOTO: Not every mathematician hates theorem provers. Timothy Gowers, of the University of Cambridge, thinks they may one day replace human reviewers at mathematical journals. The Abel Prize
———————-
With an ATP, a programmer can code in all the rules, or axioms, and then ask if a particular conjecture follows those rules. The computer then does all the work. “You just type in the conjecture you want to prove, and you hope you get an answer,” said Daniel Huang, a computer scientist who recently left the University of California, Berkeley, to work at a startup.
But here’s the rub: What an ATP doesn’t do is explain its work. All that calculating happens within the machine, and to human eyes it would look like a long string of 0s and 1s. Huang said it’s impossible to scan the proof and follow the reasoning, because it looks like a pile of random data. “No human will ever look at that proof and be able to say, ‘I get it,'” he said.
ITPs, the second category, have vast data sets containing up to tens of thousands of theorems and proofs, which they can scan to verify that a proof is accurate. Unlike ATPs, which operate in a kind of black box and just spit out an answer, ITPs require human interaction and even guidance along the way, so they’re not as inaccessible. “A human could sit down and understand what the proof-level techniques are,” said Huang. (These are the kinds of machine proofs DeDeo and Viteri studied.)
ITPs have become increasingly popular in recent years. In 2017, the trio behind the Boolean Pythagorean triples problem used Coq, an ITP, to create and verify a formal version of their proof; in 2005 Georges Gonthier at Microsoft Research Cambridge used Coq to formalize the four-color theorem. Hales also used ITPs called HOL Light and Isabelle on the formal proof of the Kepler conjecture. (“HOL” stands for “higher-order logic.”)
Efforts at the forefront of the field today aim to blend learning with reasoning. They often combine ATPs with ITPs and also integrate machine learning tools to improve the efficiency of both. They envision ATP/ITP programs that can use deductive reasoning – and even communicate mathematical ideas – the same way people do, or at least in similar ways.
The Limits of Reason
Josef Urban thinks that the marriage of deductive and inductive reasoning required for proofs can be achieved through this kind of combined approach. His group has built theorem provers guided by machine learning tools, which allow computers to learn on their own through experience. Over the last few years, they’ve explored the use of neural networks – layers of computations that help machines process information through a rough approximation of our brain’s neuronal activity. In July, his group reported on new conjectures generated by a neural network trained on theorem-proving data.
Urban was partially inspired by Andrej Karpathy, who a few years ago trained a neural network to generate mathematical-looking nonsense that looked legitimate to nonexperts. Urban didn’t want nonsense, though – he and his group instead designed their own tool to find new proofs after training on millions of theorems. Then they used the network to generate new conjectures and checked the validity of those conjectures using an ATP called E.
The network proposed more than 50,000 new formulas, though tens of thousands were duplicates. “It seems that we are not yet capable of proving the more interesting conjectures,” Urban said.
————————–
SIDEBAR: [Machines] will learn how to do their own prompts. Timothy Gowers, University of Cambridge
—————————-
Szegedy at Google Research sees the challenge of automating reasoning in computer proofs as a subset of a much bigger field: natural language processing, which involves pattern recognition in the usage of words and sentences. (Pattern recognition is also the driving idea behind computer vision, the object of Szegedy’s previous project at Google.) Like other groups, his team wants theorem provers that can find and explain useful proofs.
Inspired by the rapid development of AI tools like AlphaZero – the DeepMind program that can defeat humans at chess, Go and shogi – Szegedy’s group wants to capitalize on recent advances in language recognition to write proofs. Language models, he said, can demonstrate surprisingly solid mathematical reasoning.
His group at Google Research recently described a way to use language models – which often use neural networks – to generate new proofs. After training the model to recognize a kind of treelike structure in theorems that are known to be true, they ran a kind of free-form experiment, simply asking the network to generate and prove a theorem without any further guidance. Of the thousands of generated conjectures, about 13% were both provable and new (meaning they didn’t duplicate other theorems in the database). The experiment, he said, suggests that the neural net could teach itself a kind of understanding of what a proof looks like.
“Neural networks are able to develop an artificial style of intuition,” Szegedy said.
Of course, it’s still unclear whether these efforts will fulfill Cohen’s prophecy from over 40 years ago. Gowers has said that he thinks computers will be able to out-reason mathematicians by 2099. At first, he predicts, mathematicians will enjoy a kind of golden age, “when mathematicians do all the fun parts and computers do all the boring parts. But I think it will last a very short time.”
Harris disagrees. He doesn’t think computer provers are necessary, or that they will inevitably “make human mathematicians obsolete.” If computer scientists are ever able to program a kind of synthetic intuition, he says, it still won’t rival that of humans. “Even if computers understand, they don’t understand in a human way.”
Here is some information that teachers at quite a few different levels could use* for a really interesting geometry lesson involving reflections involving two or more mirrors, placed at various angles!
Certain specific angles have very special effects, including 90, 72, 60, 45 degrees … But WHY?
This could be done with actual mirrors and a protractor, or with geometry software like Geometer’s Sketchpad or Desmos. Students could also end up making their own kaleidoscopes – either with little bits of colored plastic at the end or else with some sort of a wide-angle lens. (You can find many easy directions online for doing just that; some kits are a lot more optically perfect than others, but I don’t think I’ve even seen a kaleidoscope that had its mirrors set at any angle other than 60 degrees!)
I am reproducing a couple of the images and text that Angel Gilding provides on their website(which they set up to sell silvering kits (about which I’ve posted before, and which I am going to attempt using pretty soon)).
At 72º you see 4 complete reflections.
When two mirrors are parallel to each other, the number of reflections is infinite. Placing one mirror at a slight angle causes the reflections to curve.
* assuming that the teacher are still allowed to initiate and carry out interesting projects for their students to use, and aren’t forced to follow a scripted curriculum. It would be a lot better use of computers than forcing kids to painfully walk through (and cheat, and goof off a lot) when an entire class is forced to use one of those very expensive but basically worthless highly-centralized, district-purchased computer-managed-instruction apps. God, what a waste of time – from personal experience attempting to be a volunteer community math tutor at such a school, and also from my experience as a paid or volunteer tutor in helping many many students who have had to use such programs as homework. Also when I was required to use them in my own classes, over a decade ago, I and most of my colleagues found them a waste of time. (Not all – I got officially reprimanded for telling my department chair that ‘Renaissance Math’ was either a ‘pile of crap’ or a ‘pile of shit’ to my then-department head, in the hearing of one of the APs, on a teacher-only day.
Keep in mind: I’m no Luddite! I realized early on that in math, science, and art, computers would be very, very useful. I learned how to write programs in BASIC on one of the very first time-share networks, 45 years ago. For the first ten years that my school system there was almost no decent useful software for math teachers to use with their classes unless you had AppleII computers. We had Commodore-64’s which were totally incompatible and there were very few companies (Sunburst was one) putting out any decent software for the latter. So when I saw some great ideas that would be ideal for kids to use on computers to make thinking about numbers, graphs, and equations actually fun and mentally engaging, often I would have to write them my self during whatever free time I could catch, at nights and weekends. Of course, doing this while being a daddy to 2 kids, and still trying to teach JHS math to a full load of students (100 to 150 different kids a day at Francis Junior High School) and running a school math club and later coaching soccer. (I won’t say I was a perfect person or a perfect teacher. I believe I learned to give better math explanations than most, didn’t believe that you either have a ‘m,ath gene’ or you don’t, at times had some interesting projects, and at times was very patient and clear, but had a terrible temper and often not good at defusing things. Ask my kids or my former students!) Later on, I collaborated with some French math teachers and a computer programmer to try to make an app/program called Geometrix for American geometry classes that was supposed to help kids figure out how to make all sorts of geometric constructions and then develop a proof of some property of that situation. It was a failure. I was the one writing the American version, including constructions and tasks from the text I was currently using. There was no way I could anticipate what sorts of obstacles students would find when using this program, until I had actual guinea pig students to use them with. Turns out the final crunch of writing however many hundreds of exercises took place over the summer, and no students to try them on. Figuring out hints and clues would require watching a whole bunch of kids and seeing what they were getting right or wrong. In other words, a lot of people’s full time job for a long time, maybe paying the kids as well to try it out so as to get good feedback, and so on. Maybe it could work, but it would require a lot more investment of resources that the tiny French and American companies involved could afford. We would have really needed a team of people, not just me and a single checker.
I find that none of these computer-dominated online learning programs (much less the one I worked on) can take the place of a good teacher. Being in class, listening to and communicating logically or emotionally with a number of other students and a knowledgeable adult or two, is in itself an extremely important skill to learn. It’s also the best way to absorb new material in a way that will make sense and be added to one’s store of knowledge. That sort of group interaction is simply IMPOSSIBLE in a class where everybody is completely atomized and is on their own electronic device, engaged or not.
Without a human being trying to make sense out of the material, what I found quite consistently, in all the computerized settings, that most students absorbed nothing at all or else the wrong lessons altogether (such as, ‘if you randomly try all the multiple choice answers, you’ll eventually pick the right one and you can move on to some other stupid screen’; it doesn’t matter that all your prior choices were wrong; sometimes you get lucky and pick the right one first or second! Whee! It’s like a slot machine at a casino!).
By contrast, I found that with programs/apps/languages like Logo, Darts, Green Globs, or Geometer’s Sketchpad, with teacher guidance, students actually got engaged in the process, had fun, and learned something.
I find the canned computer “explanations” are almost always ignored by the students, and are sometimes flat-out wrong. Other times, although they may be mathematically correct, they assume either way too much or way too little, or else are just plain confusing. I have yet to detect much of any learning going on because of those programs.
I thought I would share the URLs of a number of commercial establishments that offer astronomical viewing with very dark skies. Most of these are located in or near New Mexico.
Source: Lynn Rice of New Mexico Skies, which now (sadly) only does remote hosting — in other words, people far away use the telescopes at NMS via fast internet connections, for a fee.
New Mexico Skies, Inc.
9 Contentment Crest #182
Mayhill NM 88339
Guy's Math & Astro Blog 